Theorem: SetTheory.interpret_eqEmpty (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqEmpty x) v l ↔ interpretTerm V v l x = ∅
Tactic:
unfold BoundedFormula.eqEmpty
State after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    interpretTerm V v l x = ∅

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    interpretTerm V v l x = ∅
Tactic:
rw [eq_empty_iff_forall_not_mem]
State after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    ∀ (y : V), ¬y ∈ interpretTerm V v l x

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.all (BoundedFormula.not (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x)))) v l ↔
    ∀ (y : V), ¬y ∈ interpretTerm V v l x
Tactic:
simp
State after:
no goals