Metamath Proof Explorer

Theorem eliminable-abeqv

Description: A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals variable. (Contributed by BJ, 30-Apr-2024) Beware not to use symmetry of class equality. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion eliminable-abeqv ⊢ x | φ = y ↔ ∀ z z x φ ↔ z ∈ y

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ x | φ = y ↔ ∀ z z ∈ x | φ ↔ z ∈ y
2 eliminable-velab ⊢ z ∈ x | φ ↔ z x φ
3 2 bibi1i ⊢ z ∈ x | φ ↔ z ∈ y ↔ z x φ ↔ z ∈ y
4 3 albii ⊢ ∀ z z ∈ x | φ ↔ z ∈ y ↔ ∀ z z x φ ↔ z ∈ y
5 1 4 bitri ⊢ x | φ = y ↔ ∀ z z x φ ↔ z ∈ y