# Metamath Proof Explorer

## Theorem sbccow

Description: A composition law for class substitution. Version of sbcco with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 26-Sep-2003) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Assertion sbccow
`|- ( [. 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 sbco2vv
` |-  ( [ z / y ] [ y / x ] ph <-> [ z / x ] ph )`
8 sbsbc
` |-  ( [ z / y ] [. y / x ]. ph <-> [. z / y ]. [. y / x ]. ph )`
9 6 7 8 3bitr3ri
` |-  ( [. z / y ]. [. y / x ]. ph <-> [ z / x ] ph )`
10 sbsbc
` |-  ( [ z / x ] ph <-> [. z / x ]. ph )`
11 9 10 bitri
` |-  ( [. z / y ]. [. y / x ]. ph <-> [. z / x ]. ph )`
12 3 4 11 vtoclbg
` |-  ( A e. _V -> ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph ) )`
13 1 2 12 pm5.21nii
` |-  ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )`