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=yA=B
Assertion sbcco2 [˙x/y]˙[˙B/x]˙φ[˙A/x]˙φ

Proof

Step Hyp Ref Expression
1 sbcco2.1 x=yA=B
2 sbsbc xy[˙B/x]˙φ[˙x/y]˙[˙B/x]˙φ
3 1 equcoms y=xA=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 xy[˙B/x]˙φ[˙A/x]˙φ
8 2 7 bitr3i [˙x/y]˙[˙B/x]˙φ[˙A/x]˙φ