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

Metamath Proof Explorer

Theorem elssabg

Description: Membership in a class abstraction involving a subset. Unlike elabg , A does not have to be a set. (Contributed by NM, 29-Aug-2006)

Ref Expression
Hypothesis elssabg.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion elssabg 
|- ( B e. V -> ( A e. { x | ( x C_ B /\ ph ) } <-> ( A C_ B /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 elssabg.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
3 2 expcom 
 |-  ( B e. V -> ( A C_ B -> A e. _V ) )
4 3 adantrd 
 |-  ( B e. V -> ( ( A C_ B /\ ps ) -> A e. _V ) )
5 sseq1 
 |-  ( x = A -> ( x C_ B <-> A C_ B ) )
6 5 1 anbi12d 
 |-  ( x = A -> ( ( x C_ B /\ ph ) <-> ( A C_ B /\ ps ) ) )
7 6 elab3g 
 |-  ( ( ( A C_ B /\ ps ) -> A e. _V ) -> ( A e. { x | ( x C_ B /\ ph ) } <-> ( A C_ B /\ ps ) ) )
8 4 7 syl 
 |-  ( B e. V -> ( A e. { x | ( x C_ B /\ ph ) } <-> ( A C_ B /\ ps ) ) )