Metamath Proof Explorer

Theorem clel2gOLD

Description: Obsolete version of clel2g as of 1-Sep-2024. (Contributed by NM, 18-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion clel2gOLD 
|- ( A e. V -> ( A e. B <-> A. x ( x = A -> x e. B ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x A e. B
2 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
3 1 2 ceqsalg 
 |-  ( A e. V -> ( A. x ( x = A -> x e. B ) <-> A e. B ) )
4 3 bicomd 
 |-  ( A e. V -> ( A e. B <-> A. x ( x = A -> x e. B ) ) )