Description: Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | ichal | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-11 | |
|
2 | ax-11 | |
|
3 | 2 | alimi | |
4 | sbal | |
|
5 | 4 | 2sbbii | |
6 | sbal | |
|
7 | 6 | sbbii | |
8 | sbal | |
|
9 | 5 7 8 | 3bitri | |
10 | albi | |
|
11 | 9 10 | bitrid | |
12 | 11 | 2alimi | |
13 | 1 3 12 | 3syl | |
14 | df-ich | |
|
15 | 14 | albii | |
16 | df-ich | |
|
17 | 13 15 16 | 3imtr4i | |