Theorem cgsex2gd

Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995) Adapt cgsex2g $p to deduction form. (Revised by BJ, 28-Mar-2026) Do not use cgsex2g . (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	cgsex2gd.is	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ps )
	cgsex2gd.maj	|- ( ( ph /\ ps ) -> ( ch <-> th ) )
Assertion	cgsex2gd	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( E. x E. y ( ps /\ ch ) <-> th ) )

Proof

Step	Hyp	Ref	Expression
1		cgsex2gd.is	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ps )
2		cgsex2gd.maj	|- ( ( ph /\ ps ) -> ( ch <-> th ) )
3	2	biimp3a	|- ( ( ph /\ ps /\ ch ) -> th )
4	3	3expib	|- ( ph -> ( ( ps /\ ch ) -> th ) )
5	4	exlimdvv	|- ( ph -> ( E. x E. y ( ps /\ ch ) -> th ) )
6	5	adantr	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( E. x E. y ( ps /\ ch ) -> th ) )
7	1	ex	|- ( ph -> ( ( x = A /\ y = B ) -> ps ) )
8	7	2eximdv	|- ( ph -> ( E. x E. y ( x = A /\ y = B ) -> E. x E. y ps ) )
9		elisset	|- ( A e. V -> E. x x = A )
10		elisset	|- ( B e. W -> E. y y = B )
11	9 10	anim12i	|- ( ( A e. V /\ B e. W ) -> ( E. x x = A /\ E. y y = B ) )
12		exdistrv	|- ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
13	11 12	sylibr	|- ( ( A e. V /\ B e. W ) -> E. x E. y ( x = A /\ y = B ) )
14	8 13	impel	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> E. x E. y ps )
15	2	biimprd	|- ( ( ph /\ ps ) -> ( th -> ch ) )
16	15	impancom	|- ( ( ph /\ th ) -> ( ps -> ch ) )
17	16	ancld	|- ( ( ph /\ th ) -> ( ps -> ( ps /\ ch ) ) )
18	17	2eximdv	|- ( ( ph /\ th ) -> ( E. x E. y ps -> E. x E. y ( ps /\ ch ) ) )
19	18	expimpd	|- ( ph -> ( ( th /\ E. x E. y ps ) -> E. x E. y ( ps /\ ch ) ) )
20	19	adantr	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( ( th /\ E. x E. y ps ) -> E. x E. y ( ps /\ ch ) ) )
21	14 20	mpan2d	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( th -> E. x E. y ( ps /\ ch ) ) )
22	6 21	impbid	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( E. x E. y ( ps /\ ch ) <-> th ) )