Metamath Proof Explorer

Theorem clelabOLD

Description: Obsolete version of clelab as of 2-Sep-2024. (Contributed by NM, 23-Dec-1993) (Proof shortened by Wolf Lammen, 16-Nov-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion clelabOLD ⊢ A ∈ x | φ ↔ ∃ x x = A ∧ φ

Proof

Step Hyp Ref Expression
1 dfclel ⊢ A ∈ x | φ ↔ ∃ y y = A ∧ y ∈ x | φ
2 nfv ⊢ Ⅎ y x = A ∧ φ
3 nfv ⊢ Ⅎ x y = A
4 nfsab1 ⊢ Ⅎ x y ∈ x | φ
5 3 4 nfan ⊢ Ⅎ x y = A ∧ y ∈ x | φ
6 eqeq1 ⊢ x = y → x = A ↔ y = A
7 sbequ12 ⊢ x = y → φ ↔ y x φ
8 df-clab ⊢ y ∈ x | φ ↔ y x φ
9 7 8 bitr4di ⊢ x = y → φ ↔ y ∈ x | φ
10 6 9 anbi12d ⊢ x = y → x = A ∧ φ ↔ y = A ∧ y ∈ x | φ
11 2 5 10 cbvexv1 ⊢ ∃ x x = A ∧ φ ↔ ∃ y y = A ∧ y ∈ x | φ
12 1 11 bitr4i ⊢ A ∈ x | φ ↔ ∃ x x = A ∧ φ