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

Metamath Proof Explorer

Theorem sbco2

Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v and sbco2vv . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 30-Jun-1994) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 17-Sep-2018) (New usage is discouraged.)

Ref Expression
Hypothesis sbco2.1 
|- F/ z ph
Assertion sbco2 
|- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )

Proof

Step Hyp Ref Expression
1 sbco2.1 
 |-  F/ z ph
2 sbequ12 
 |-  ( z = y -> ( [ z / x ] ph <-> [ y / z ] [ z / x ] ph ) )
3 sbequ 
 |-  ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
4 2 3 bitr3d 
 |-  ( z = y -> ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) )
5 4 sps 
 |-  ( A. z z = y -> ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) )
6 nfnae 
 |-  F/ z -. A. z z = y
7 1 nfsb4 
 |-  ( -. A. z z = y -> F/ z [ y / x ] ph )
8 3 a1i 
 |-  ( -. A. z z = y -> ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) ) )
9 6 7 8 sbied 
 |-  ( -. A. z z = y -> ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) )
10 5 9 pm2.61i 
 |-  ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )