# Metamath Proof Explorer

## Theorem sbcco

Description: A composition law for class substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbccow when possible. (Contributed by NM, 26-Sep-2003) (Revised by Mario Carneiro, 13-Oct-2016) (New usage is discouraged.)

Ref Expression
Assertion sbcco
`|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )`

### Proof

Step Hyp Ref Expression
1 sbcex
` |-  ( [. A / y ]. [. y / x ]. ph -> A e. _V )`
2 sbcex
` |-  ( [. A / x ]. ph -> A e. _V )`
3 dfsbcq
` |-  ( z = A -> ( [. z / y ]. [. y / x ]. ph <-> [. A / y ]. [. y / x ]. ph ) )`
4 dfsbcq
` |-  ( z = A -> ( [. z / x ]. ph <-> [. A / x ]. ph ) )`
5 sbsbc
` |-  ( [ y / x ] ph <-> [. y / x ]. ph )`
6 5 sbbii
` |-  ( [ z / y ] [ y / x ] ph <-> [ z / y ] [. y / x ]. ph )`
7 nfv
` |-  F/ y ph`
8 7 sbco2
` |-  ( [ z / y ] [ y / x ] ph <-> [ z / x ] ph )`
9 sbsbc
` |-  ( [ z / y ] [. y / x ]. ph <-> [. z / y ]. [. y / x ]. ph )`
10 6 8 9 3bitr3ri
` |-  ( [. z / y ]. [. y / x ]. ph <-> [ z / x ] ph )`
11 sbsbc
` |-  ( [ z / x ] ph <-> [. z / x ]. ph )`
12 10 11 bitri
` |-  ( [. z / y ]. [. y / x ]. ph <-> [. z / x ]. ph )`
13 3 4 12 vtoclbg
` |-  ( A e. _V -> ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph ) )`
14 1 2 13 pm5.21nii
` |-  ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )`