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 ⊢ 𝐴 ∈ V
vtoclb.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
vtoclb.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
vtoclb.4 ⊢ ( 𝜑 ↔ 𝜓 )
Assertion vtoclb ( 𝜒 ↔ 𝜃 )

Proof

Step Hyp Ref Expression
1 vtoclb.1 ⊢ 𝐴 ∈ V
2 vtoclb.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
3 vtoclb.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
4 vtoclb.4 ⊢ ( 𝜑 ↔ 𝜓 )
5 2 3 bibi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜒 ↔ 𝜃 ) ) )
6 1 5 4 vtocl ⊢ ( 𝜒 ↔ 𝜃 )