Description: Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in Jech p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | opthprc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 | |
|
2 | 0ex | |
|
3 | 2 | snid | |
4 | opelxp | |
|
5 | 3 4 | mpbiran2 | |
6 | opelxp | |
|
7 | 0nep0 | |
|
8 | 2 | elsn | |
9 | 7 8 | nemtbir | |
10 | 9 | bianfi | |
11 | 6 10 | bitr4i | |
12 | 5 11 | orbi12i | |
13 | elun | |
|
14 | 9 | biorfi | |
15 | 12 13 14 | 3bitr4ri | |
16 | opelxp | |
|
17 | 3 16 | mpbiran2 | |
18 | opelxp | |
|
19 | 9 | bianfi | |
20 | 18 19 | bitr4i | |
21 | 17 20 | orbi12i | |
22 | elun | |
|
23 | 9 | biorfi | |
24 | 21 22 23 | 3bitr4ri | |
25 | 1 15 24 | 3bitr4g | |
26 | 25 | eqrdv | |
27 | eleq2 | |
|
28 | opelxp | |
|
29 | snex | |
|
30 | 29 | elsn | |
31 | eqcom | |
|
32 | 30 31 | bitri | |
33 | 7 32 | nemtbir | |
34 | 33 | bianfi | |
35 | 28 34 | bitr4i | |
36 | 29 | snid | |
37 | opelxp | |
|
38 | 36 37 | mpbiran2 | |
39 | 35 38 | orbi12i | |
40 | elun | |
|
41 | biorf | |
|
42 | 33 41 | ax-mp | |
43 | 39 40 42 | 3bitr4ri | |
44 | opelxp | |
|
45 | 33 | bianfi | |
46 | 44 45 | bitr4i | |
47 | opelxp | |
|
48 | 36 47 | mpbiran2 | |
49 | 46 48 | orbi12i | |
50 | elun | |
|
51 | biorf | |
|
52 | 33 51 | ax-mp | |
53 | 49 50 52 | 3bitr4ri | |
54 | 27 43 53 | 3bitr4g | |
55 | 54 | eqrdv | |
56 | 26 55 | jca | |
57 | xpeq1 | |
|
58 | xpeq1 | |
|
59 | uneq12 | |
|
60 | 57 58 59 | syl2an | |
61 | 56 60 | impbii | |