Metamath Proof Explorer


Theorem sbcom3

Description: Substituting y for x and then z for y is equivalent to substituting z for both x and y . Usage of this theorem is discouraged because it depends on ax-13 . For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv . (Contributed by Giovanni Mascellani, 8-Apr-2018) Remove dependency on ax-11 . (Revised by Wolf Lammen, 16-Sep-2018) (Proof shortened by Wolf Lammen, 16-Sep-2018) (New usage is discouraged.)

Ref Expression
Assertion sbcom3
|- ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph )

Proof

Step Hyp Ref Expression
1 nfa1
 |-  F/ y A. y y = z
2 drsb2
 |-  ( A. y y = z -> ( [ y / x ] ph <-> [ z / x ] ph ) )
3 1 2 sbbid
 |-  ( A. y y = z -> ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph ) )
4 sb4b
 |-  ( -. A. y y = z -> ( [ z / y ] [ y / x ] ph <-> A. y ( y = z -> [ y / x ] ph ) ) )
5 sbequ
 |-  ( y = z -> ( [ y / x ] ph <-> [ z / x ] ph ) )
6 5 pm5.74i
 |-  ( ( y = z -> [ y / x ] ph ) <-> ( y = z -> [ z / x ] ph ) )
7 6 albii
 |-  ( A. y ( y = z -> [ y / x ] ph ) <-> A. y ( y = z -> [ z / x ] ph ) )
8 4 7 bitrdi
 |-  ( -. A. y y = z -> ( [ z / y ] [ y / x ] ph <-> A. y ( y = z -> [ z / x ] ph ) ) )
9 sb4b
 |-  ( -. A. y y = z -> ( [ z / y ] [ z / x ] ph <-> A. y ( y = z -> [ z / x ] ph ) ) )
10 8 9 bitr4d
 |-  ( -. A. y y = z -> ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph ) )
11 3 10 pm2.61i
 |-  ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph )