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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sb | |
|
2 | 19.23v | |
|
3 | ax6ev | |
|
4 | pm2.27 | |
|
5 | 3 4 | ax-mp | |
6 | ax-1 | |
|
7 | 5 6 | impbii | |
8 | 2 7 | bitri | |
9 | 8 | imbi2i | |
10 | 9 | albii | |
11 | 19.23v | |
|
12 | ax6ev | |
|
13 | pm2.27 | |
|
14 | 12 13 | ax-mp | |
15 | ax-1 | |
|
16 | 14 15 | impbii | |
17 | 11 16 | bitri | |
18 | 10 17 | bitri | |
19 | 1 18 | bitri | |