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

Metamath Proof Explorer

Theorem sbcbi1

Description: Distribution of class substitution over biconditional. One direction of sbcbig that holds for proper classes. (Contributed by NM, 17-Aug-2018)

Ref Expression
Assertion sbcbi1 ⊢ [˙A / x]˙ φ ↔ ψ → [˙A / x]˙ φ ↔ [˙A / x]˙ ψ

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / x]˙ φ ↔ ψ → A ∈ V
2 sbcbig ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ ↔ [˙A / x]˙ φ ↔ [˙A / x]˙ ψ
3 2 biimpd ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ → [˙A / x]˙ φ ↔ [˙A / x]˙ ψ
4 1 3 mpcom ⊢ [˙A / x]˙ φ ↔ ψ → [˙A / x]˙ φ ↔ [˙A / x]˙ ψ