Theorem vtocl3g

Description: Implicit substitution of a class for a setvar variable. Version of vtocl3gf with disjoint variable conditions instead of nonfreeness hypotheses, requiring fewer axioms. (Contributed by Gino Giotto, 3-Oct-2024)

	Ref	Expression
Hypotheses	vtocl3g.1	|- ( x = A -> ( ph <-> ps ) )
	vtocl3g.2	|- ( y = B -> ( ps <-> ch ) )
	vtocl3g.3	|- ( z = C -> ( ch <-> th ) )
	vtocl3g.4	|- ph
Assertion	vtocl3g	|- ( ( A e. V /\ B e. W /\ C e. X ) -> th )

Proof

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