Theorem vtocldf

Description: Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	vtocld.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	vtocld.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
	vtocld.3	⊢ ( 𝜑 → 𝜓 )
	vtocldf.4	⊢ Ⅎ 𝑥 𝜑
	vtocldf.5	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	vtocldf.6	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
Assertion	vtocldf	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocld.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		vtocld.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
3		vtocld.3	⊢ ( 𝜑 → 𝜓 )
4		vtocldf.4	⊢ Ⅎ 𝑥 𝜑
5		vtocldf.5	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
6		vtocldf.6	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
7	2	ex	⊢ ( 𝜑 → ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
8	4 7	alrimi	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) ) )
9	4 3	alrimi	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
10		vtoclgft	⊢ ( ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜒 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) ) ∧ ∀ 𝑥 𝜓 ) ∧ 𝐴 ∈ 𝑉 ) → 𝜒 )
11	5 6 8 9 1 10	syl221anc	⊢ ( 𝜑 → 𝜒 )