Theorem cgsex2g

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995)

	Ref	Expression
Hypotheses	cgsex2g.1	|- ( ( x = A /\ y = B ) -> ch )
	cgsex2g.2	|- ( ch -> ( ph <-> ps ) )
Assertion	cgsex2g	|- ( ( A e. V /\ B e. W ) -> ( E. x E. y ( ch /\ ph ) <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		cgsex2g.1	|- ( ( x = A /\ y = B ) -> ch )
2		cgsex2g.2	|- ( ch -> ( ph <-> ps ) )
3	2	biimpa	|- ( ( ch /\ ph ) -> ps )
4	3	exlimivv	|- ( E. x E. y ( ch /\ ph ) -> ps )
5		elisset	|- ( A e. V -> E. x x = A )
6		elisset	|- ( B e. W -> E. y y = B )
7	5 6	anim12i	|- ( ( A e. V /\ B e. W ) -> ( E. x x = A /\ E. y y = B ) )
8		exdistrv	|- ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
9	7 8	sylibr	|- ( ( A e. V /\ B e. W ) -> E. x E. y ( x = A /\ y = B ) )
10	1	2eximi	|- ( E. x E. y ( x = A /\ y = B ) -> E. x E. y ch )
11	9 10	syl	|- ( ( A e. V /\ B e. W ) -> E. x E. y ch )
12	2	biimprcd	|- ( ps -> ( ch -> ph ) )
13	12	ancld	|- ( ps -> ( ch -> ( ch /\ ph ) ) )
14	13	2eximdv	|- ( ps -> ( E. x E. y ch -> E. x E. y ( ch /\ ph ) ) )
15	11 14	syl5com	|- ( ( A e. V /\ B e. W ) -> ( ps -> E. x E. y ( ch /\ ph ) ) )
16	4 15	impbid2	|- ( ( A e. V /\ B e. W ) -> ( E. x E. y ( ch /\ ph ) <-> ps ) )