Description: An equivalent definition of df-mpo . (Contributed by BJ, 30-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-dfmpoa | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpo | |
|
2 | dfoprab2 | |
|
3 | ancom | |
|
4 | 3 | anbi2i | |
5 | anass | |
|
6 | an13 | |
|
7 | 4 5 6 | 3bitr2i | |
8 | 7 | exbii | |
9 | df-rex | |
|
10 | r19.42v | |
|
11 | 8 9 10 | 3bitr2i | |
12 | 11 | exbii | |
13 | df-rex | |
|
14 | 12 13 | bitr4i | |
15 | 14 | opabbii | |
16 | 1 2 15 | 3eqtri | |