Metamath Proof Explorer

Theorem sbcom2

Description: Commutativity law for substitution. Used in proof of Theorem 9.7 of Megill p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997) (Proof shortened by Wolf Lammen, 23-Dec-2022)

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

Proof

Step Hyp Ref Expression
1 2sb6 
 |-  ( [ v / z ] [ u / x ] ph <-> A. z A. x ( ( z = v /\ x = u ) -> ph ) )
2 alcom 
 |-  ( A. z A. x ( ( z = v /\ x = u ) -> ph ) <-> A. x A. z ( ( z = v /\ x = u ) -> ph ) )
3 ancomst 
 |-  ( ( ( z = v /\ x = u ) -> ph ) <-> ( ( x = u /\ z = v ) -> ph ) )
4 3 2albii 
 |-  ( A. x A. z ( ( z = v /\ x = u ) -> ph ) <-> A. x A. z ( ( x = u /\ z = v ) -> ph ) )
5 1 2 4 3bitri 
 |-  ( [ v / z ] [ u / x ] ph <-> A. x A. z ( ( x = u /\ z = v ) -> ph ) )
6 2sb6 
 |-  ( [ u / x ] [ v / z ] ph <-> A. x A. z ( ( x = u /\ z = v ) -> ph ) )
7 5 6 bitr4i 
 |-  ( [ v / z ] [ u / x ] ph <-> [ u / x ] [ v / z ] ph )
8 sbequ 
 |-  ( u = y -> ( [ u / x ] ph <-> [ y / x ] ph ) )
9 8 sbbidv 
 |-  ( u = y -> ( [ v / z ] [ u / x ] ph <-> [ v / z ] [ y / x ] ph ) )
10 7 9 bitr3id 
 |-  ( u = y -> ( [ u / x ] [ v / z ] ph <-> [ v / z ] [ y / x ] ph ) )
11 sbequ 
 |-  ( v = w -> ( [ v / z ] [ y / x ] ph <-> [ w / z ] [ y / x ] ph ) )
12 10 11 sylan9bb 
 |-  ( ( u = y /\ v = w ) -> ( [ u / x ] [ v / z ] ph <-> [ w / z ] [ y / x ] ph ) )
13 sbequ 
 |-  ( v = w -> ( [ v / z ] ph <-> [ w / z ] ph ) )
14 13 sbbidv 
 |-  ( v = w -> ( [ u / x ] [ v / z ] ph <-> [ u / x ] [ w / z ] ph ) )
15 sbequ 
 |-  ( u = y -> ( [ u / x ] [ w / z ] ph <-> [ y / x ] [ w / z ] ph ) )
16 14 15 sylan9bbr 
 |-  ( ( u = y /\ v = w ) -> ( [ u / x ] [ v / z ] ph <-> [ y / x ] [ w / z ] ph ) )
17 12 16 bitr3d 
 |-  ( ( u = y /\ v = w ) -> ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph ) )
18 17 ex 
 |-  ( u = y -> ( v = w -> ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph ) ) )
19 ax6ev 
 |-  E. u u = y
20 18 19 exlimiiv 
 |-  ( v = w -> ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph ) )
21 ax6ev 
 |-  E. v v = w
22 20 21 exlimiiv 
 |-  ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )