Theorem vtocl2d

Description: Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020) (Revised by BTernaryTau, 19-Oct-2023)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl2d.a	|- ( ph -> A e. V )
2		vtocl2d.b	|- ( ph -> B e. W )
3		vtocl2d.1	|- ( ( x = A /\ y = B ) -> ( ps <-> ch ) )
4		vtocl2d.3	|- ( ph -> ps )
5	4	adantr	|- ( ( ph /\ y = B ) -> ps )
6	3	adantll	|- ( ( ( ph /\ x = A ) /\ y = B ) -> ( ps <-> ch ) )
7	6	pm5.74da	|- ( ( ph /\ x = A ) -> ( ( y = B -> ps ) <-> ( y = B -> ch ) ) )
8	4	a1d	|- ( ph -> ( y = B -> ps ) )
9	1 7 8	vtocld	|- ( ph -> ( y = B -> ch ) )
10	9	imp	|- ( ( ph /\ y = B ) -> ch )
11	5 10	2thd	|- ( ( ph /\ y = B ) -> ( ps <-> ch ) )
12	2 11 4	vtocld	|- ( ph -> ch )