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 𝜓