Theorem vtocl3

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)

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

Proof

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