![]() |
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 4079 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 418 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 |
This theorem is referenced by: otth2 4092 opabid 4108 elopab 4109 opabm 4131 elvvv 4530 relsnop 4573 xpiindim 4604 raliunxp 4608 rexiunxp 4609 intirr 4851 xpmlem 4885 dmsnm 4930 dmsnopg 4936 cnvcnvsn 4941 op2ndb 4948 cnviinm 5006 funopg 5082 fsn 5508 fvsn 5531 idref 5574 oprabid 5719 dfoprab2 5734 rnoprab 5769 fo1st 5966 fo2nd 5967 eloprabi 6004 xporderlem 6034 cnvoprab 6037 dmtpos 6059 rntpos 6060 tpostpos 6067 iinerm 6404 th3qlem2 6435 elixpsn 6532 ensn1 6593 mapsnen 6608 xpsnen 6617 xpcomco 6622 xpassen 6626 xpmapenlem 6645 phplem2 6649 ac6sfi 6694 djuss 6841 genipdm 7172 ioof 9537 fsumcnv 10996 |
Copyright terms: Public domain | W3C validator |