Description: If A is a proper class and F is any class, then there is no unique set which is related to A through the binary relation F . See brprcneuALT for a proof that uses ax-pow instead of ax-pr . (Contributed by Scott Fenton, 7-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | brprcneu | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dtru | |
|
2 | exnal | |
|
3 | equcom | |
|
4 | 3 | albii | |
5 | 2 4 | xchbinx | |
6 | 1 5 | mpbir | |
7 | 6 | jctr | |
8 | 19.42v | |
|
9 | 7 8 | sylibr | |
10 | opprc1 | |
|
11 | 10 | eleq1d | |
12 | opprc1 | |
|
13 | 12 | eleq1d | |
14 | 11 13 | anbi12d | |
15 | anidm | |
|
16 | 14 15 | bitrdi | |
17 | 16 | anbi1d | |
18 | 17 | exbidv | |
19 | 11 18 | imbi12d | |
20 | 9 19 | mpbiri | |
21 | df-br | |
|
22 | df-br | |
|
23 | 21 22 | anbi12i | |
24 | 23 | anbi1i | |
25 | 24 | exbii | |
26 | 20 21 25 | 3imtr4g | |
27 | 26 | eximdv | |
28 | exnal | |
|
29 | exanali | |
|
30 | 29 | exbii | |
31 | breq2 | |
|
32 | 31 | mo4 | |
33 | 32 | notbii | |
34 | 28 30 33 | 3bitr4ri | |
35 | 27 34 | imbitrrdi | |
36 | df-eu | |
|
37 | 36 | notbii | |
38 | imnan | |
|
39 | 37 38 | bitr4i | |
40 | 35 39 | sylibr | |