This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtoclf

Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar . (Contributed by NM, 30-Aug-1993) (Proof shortened by Wolf Lammen, 26-Jan-2025)

	Ref	Expression
Hypotheses	vtoclf.1	⊢ Ⅎ 𝑥 𝜓
	vtoclf.2	⊢ 𝐴 ∈ V
	vtoclf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtoclf.4	⊢ 𝜑
Assertion	vtoclf	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		vtoclf.1	⊢ Ⅎ 𝑥 𝜓
2		vtoclf.2	⊢ 𝐴 ∈ V
3		vtoclf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		vtoclf.4	⊢ 𝜑
5	4 3	mpbii	⊢ ( 𝑥 = 𝐴 → 𝜓 )
6	1 2 5	vtoclef	⊢ 𝜓