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

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 → χ ↔ θ