Metamath Proof Explorer


Theorem bj-ssbeq

Description: Substitution in an equality, disjoint variables case. Uses only ax-1 through ax-6 . It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq first with a DV condition on x , t , and then in the general case. (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ssbeq txy=zy=z

Proof

Step Hyp Ref Expression
1 df-sb txy=zuu=txx=uy=z
2 19.23v xx=uy=zxx=uy=z
3 ax6ev xx=u
4 pm2.27 xx=uxx=uy=zy=z
5 3 4 ax-mp xx=uy=zy=z
6 ax-1 y=zxx=uy=z
7 5 6 impbii xx=uy=zy=z
8 2 7 bitri xx=uy=zy=z
9 8 imbi2i u=txx=uy=zu=ty=z
10 9 albii uu=txx=uy=zuu=ty=z
11 19.23v uu=ty=zuu=ty=z
12 ax6ev uu=t
13 pm2.27 uu=tuu=ty=zy=z
14 12 13 ax-mp uu=ty=zy=z
15 ax-1 y=zuu=ty=z
16 14 15 impbii uu=ty=zy=z
17 11 16 bitri uu=ty=zy=z
18 10 17 bitri uu=txx=uy=zy=z
19 1 18 bitri txy=zy=z