Theorem vtocl2g

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995) Remove dependency on ax-10 , ax-11 , and ax-13 . (Revised by Steven Nguyen, 29-Nov-2022)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl2g.1	|- ( x = A -> ( ph <-> ps ) )
2		vtocl2g.2	|- ( y = B -> ( ps <-> ch ) )
3		vtocl2g.3	|- ph
4		elex	|- ( A e. V -> A e. _V )
5	2	imbi2d	|- ( y = B -> ( ( A e. _V -> ps ) <-> ( A e. _V -> ch ) ) )
6	1 3	vtoclg	|- ( A e. _V -> ps )
7	5 6	vtoclg	|- ( B e. W -> ( A e. _V -> ch ) )
8	4 7	mpan9	|- ( ( A e. V /\ B e. W ) -> ch )