This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clelab

Description: Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993) (Proof shortened by Wolf Lammen, 16-Nov-2019) Avoid ax-11 , see sbc5ALT for more details. (Revised by SN, 2-Sep-2024)

Ref Expression
Assertion clelab 
|- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )

Proof

Step Hyp Ref Expression
1 elissetv 
 |-  ( A e. { x | ph } -> E. y y = A )
2 exsimpl 
 |-  ( E. x ( x = A /\ ph ) -> E. x x = A )
3 iseqsetv-cleq 
 |-  ( E. x x = A <-> E. y y = A )
4 2 3 sylib 
 |-  ( E. x ( x = A /\ ph ) -> E. y y = A )
5 eleq1 
 |-  ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
6 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
7 sb5 
 |-  ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
8 6 7 bitri 
 |-  ( y e. { x | ph } <-> E. x ( x = y /\ ph ) )
9 eqeq2 
 |-  ( y = A -> ( x = y <-> x = A ) )
10 9 anbi1d 
 |-  ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
11 10 exbidv 
 |-  ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
12 8 11 bitrid 
 |-  ( y = A -> ( y e. { x | ph } <-> E. x ( x = A /\ ph ) ) )
13 5 12 bitr3d 
 |-  ( y = A -> ( A e. { x | ph } <-> E. x ( x = A /\ ph ) ) )
14 13 exlimiv 
 |-  ( E. y y = A -> ( A e. { x | ph } <-> E. x ( x = A /\ ph ) ) )
15 1 4 14 pm5.21nii 
 |-  ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )