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 ( 𝐴 ∈ { 𝑥𝜑 } ↔ ∃ 𝑥 ( 𝑥 = 𝐴𝜑 ) )

Proof

Step Hyp Ref Expression
1 dfclel ( 𝐴 ∈ { 𝑥𝜑 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴𝑦 ∈ { 𝑥𝜑 } ) )
2 nfv 𝑦 ( 𝑥 = 𝐴𝜑 )
3 nfv 𝑥 𝑦 = 𝐴
4 nfsab1 𝑥 𝑦 ∈ { 𝑥𝜑 }
5 3 4 nfan 𝑥 ( 𝑦 = 𝐴𝑦 ∈ { 𝑥𝜑 } )
6 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴𝑦 = 𝐴 ) )
7 sbequ12 ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
8 df-clab ( 𝑦 ∈ { 𝑥𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
9 7 8 bitr4di ( 𝑥 = 𝑦 → ( 𝜑𝑦 ∈ { 𝑥𝜑 } ) )
10 6 9 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝐴𝜑 ) ↔ ( 𝑦 = 𝐴𝑦 ∈ { 𝑥𝜑 } ) ) )
11 2 5 10 cbvexv1 ( ∃ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴𝑦 ∈ { 𝑥𝜑 } ) )
12 1 11 bitr4i ( 𝐴 ∈ { 𝑥𝜑 } ↔ ∃ 𝑥 ( 𝑥 = 𝐴𝜑 ) )