Description: The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | pwtp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velpw | |
|
2 | elun | |
|
3 | vex | |
|
4 | 3 | elpr | |
5 | 3 | elpr | |
6 | 4 5 | orbi12i | |
7 | 2 6 | bitri | |
8 | elun | |
|
9 | 3 | elpr | |
10 | 3 | elpr | |
11 | 9 10 | orbi12i | |
12 | 8 11 | bitri | |
13 | 7 12 | orbi12i | |
14 | elun | |
|
15 | sstp | |
|
16 | 13 14 15 | 3bitr4ri | |
17 | 1 16 | bitri | |
18 | 17 | eqriv | |