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

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 )