Theorem vtocl2

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Hypotheses	vtocl2.1	⊢ 𝐴 ∈ V
	vtocl2.2	⊢ 𝐵 ∈ V
	vtocl2.3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
	vtocl2.4	⊢ 𝜑
Assertion	vtocl2	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		vtocl2.1	⊢ 𝐴 ∈ V
2		vtocl2.2	⊢ 𝐵 ∈ V
3		vtocl2.3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
4		vtocl2.4	⊢ 𝜑
5	4	a1i	⊢ ( 𝑦 = 𝐵 → 𝜑 )
6	3	pm5.74da	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 = 𝐵 → 𝜑 ) ↔ ( 𝑦 = 𝐵 → 𝜓 ) ) )
7	1 6 5	vtocl	⊢ ( 𝑦 = 𝐵 → 𝜓 )
8	5 7	2thd	⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
9	2 8 4	vtocl	⊢ 𝜓