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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	vtocl2d.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	vtocl2d.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
	vtocl2d.3	⊢ ( 𝜑 → 𝜓 )
Assertion	vtocl2d	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocl2d.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		vtocl2d.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		vtocl2d.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
4		vtocl2d.3	⊢ ( 𝜑 → 𝜓 )
5	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝜓 )
6	3	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
7	6	pm5.74da	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑦 = 𝐵 → 𝜓 ) ↔ ( 𝑦 = 𝐵 → 𝜒 ) ) )
8	4	a1d	⊢ ( 𝜑 → ( 𝑦 = 𝐵 → 𝜓 ) )
9	1 7 8	vtocld	⊢ ( 𝜑 → ( 𝑦 = 𝐵 → 𝜒 ) )
10	9	imp	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝜒 )
11	5 10	2thd	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
12	2 11 4	vtocld	⊢ ( 𝜑 → 𝜒 )