Metamath Proof Explorer


Theorem vtoclbg

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994)

Ref Expression
Hypotheses vtoclbg.1 x = A φ χ
vtoclbg.2 x = A ψ θ
vtoclbg.3 φ ψ
Assertion vtoclbg A V χ θ

Proof

Step Hyp Ref Expression
1 vtoclbg.1 x = A φ χ
2 vtoclbg.2 x = A ψ θ
3 vtoclbg.3 φ ψ
4 1 2 bibi12d x = A φ ψ χ θ
5 4 3 vtoclg A V χ θ