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

Metamath Proof Explorer

Theorem sbcco2

Description: A composition law for class substitution. Importantly, x may occur free in the class expression substituted for A . (Contributed by NM, 5-Sep-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Hypothesis sbcco2.1 ⊢ x = y → A = B
Assertion sbcco2 ⊢ [˙x / y]˙ [˙B / x]˙ φ ↔ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbcco2.1 ⊢ x = y → A = B
2 sbsbc ⊢ x y [˙B / x]˙ φ ↔ [˙x / y]˙ [˙B / x]˙ φ
3 1 equcoms ⊢ y = x → A = B
4 dfsbcq ⊢ A = B → [˙A / x]˙ φ ↔ [˙B / x]˙ φ
5 4 bicomd ⊢ A = B → [˙B / x]˙ φ ↔ [˙A / x]˙ φ
6 3 5 syl ⊢ y = x → [˙B / x]˙ φ ↔ [˙A / x]˙ φ
7 6 sbievw ⊢ x y [˙B / x]˙ φ ↔ [˙A / x]˙ φ
8 2 7 bitr3i ⊢ [˙x / y]˙ [˙B / x]˙ φ ↔ [˙A / x]˙ φ