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

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) Avoid ax-13 . (Revised by GG, 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 )