Theorem vtocldOLD

Description: Obsolete version of vtocld as of 2-Sep-2024. (Contributed by Mario Carneiro, 15-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vtocld.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	vtocld.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
	vtocld.3	⊢ ( 𝜑 → 𝜓 )
Assertion	vtocldOLD	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocld.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		vtocld.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
3		vtocld.3	⊢ ( 𝜑 → 𝜓 )
4		nfv	⊢ Ⅎ 𝑥 𝜑
5		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
6		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
7	1 2 3 4 5 6	vtocldf	⊢ ( 𝜑 → 𝜒 )