![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opex | Unicode version |
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Ref | Expression |
---|---|
opex.1 |
![]() ![]() ![]() ![]() |
opex.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
opex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opex.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | opex.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | opexg 4240 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 426 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-pr 4221 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 |
This theorem is referenced by: otth2 4253 opabid 4269 elopab 4270 opabm 4292 elvvv 4701 relsnop 4744 xpiindim 4776 raliunxp 4780 rexiunxp 4781 intirr 5027 xpmlem 5061 dmsnm 5106 dmsnopg 5112 cnvcnvsn 5117 op2ndb 5124 cnviinm 5182 funopg 5262 fsn 5701 fvsn 5724 idref 5770 oprabid 5920 dfoprab2 5935 rnoprab 5971 fo1st 6172 fo2nd 6173 eloprabi 6211 xporderlem 6246 cnvoprab 6249 dmtpos 6271 rntpos 6272 tpostpos 6279 iinerm 6621 th3qlem2 6652 elixpsn 6749 ensn1 6810 mapsnen 6825 xpsnen 6835 xpcomco 6840 xpassen 6844 xpmapenlem 6863 phplem2 6867 ac6sfi 6912 djuss 7083 genipdm 7529 ioof 9985 fsumcnv 11459 fprodcnv 11647 prdsex 12736 txdis1cn 14074 |
Copyright terms: Public domain | W3C validator |