Theorem: SetTheory.interpret_eqSingleton (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqSingleton x y) v l ↔ interpretTerm V v l x = {interpretTerm V v l y}
Tactic:
unfold BoundedFormula.eqSingleton
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqPair x y y) v l ↔ interpretTerm V v l x = {interpretTerm V v l y}

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqPair x y y) v l ↔ interpretTerm V v l x = {interpretTerm V v l y}
Tactic:
simp
State after:
no goals