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 ) ) )