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 e. { x | ph } <-> E. x ( x = A /\ ph ) )

Proof

Step Hyp Ref Expression
1 dfclel
 |-  ( A e. { x | ph } <-> E. y ( y = A /\ y e. { x | ph } ) )
2 nfv
 |-  F/ y ( x = A /\ ph )
3 nfv
 |-  F/ x y = A
4 nfsab1
 |-  F/ x y e. { x | ph }
5 3 4 nfan
 |-  F/ x ( y = A /\ y e. { x | ph } )
6 eqeq1
 |-  ( x = y -> ( x = A <-> y = A ) )
7 sbequ12
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
8 df-clab
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
9 7 8 bitr4di
 |-  ( x = y -> ( ph <-> y e. { x | ph } ) )
10 6 9 anbi12d
 |-  ( x = y -> ( ( x = A /\ ph ) <-> ( y = A /\ y e. { x | ph } ) ) )
11 2 5 10 cbvexv1
 |-  ( E. x ( x = A /\ ph ) <-> E. y ( y = A /\ y e. { x | ph } ) )
12 1 11 bitr4i
 |-  ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )