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

Metamath Proof Explorer

Theorem vtoclb

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993)

Ref Expression
Hypotheses vtoclb.1 ⊢ A ∈ V
vtoclb.2 ⊢ x = A → φ ↔ χ
vtoclb.3 ⊢ x = A → ψ ↔ θ
vtoclb.4 ⊢ φ ↔ ψ
Assertion vtoclb ⊢ χ ↔ θ

Proof

Step Hyp Ref Expression
1 vtoclb.1 ⊢ A ∈ V
2 vtoclb.2 ⊢ x = A → φ ↔ χ
3 vtoclb.3 ⊢ x = A → ψ ↔ θ
4 vtoclb.4 ⊢ φ ↔ ψ
5 2 3 bibi12d ⊢ x = A → φ ↔ ψ ↔ χ ↔ θ
6 1 5 4 vtocl ⊢ χ ↔ θ