![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opexg | Unicode version |
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Ref | Expression |
---|---|
opexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfopg 3667 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2666 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | snexg 4066 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 14 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | adantr 272 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | elex 2666 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | prexg 4091 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 2, 6, 7 | syl2an 285 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | prexg 4091 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 5, 8, 9 | syl2anc 406 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 1, 10 | eqeltrd 2189 |
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 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-sep 4004 ax-pow 4056 ax-pr 4089 |
This theorem depends on definitions: df-bi 116 df-3an 945 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-v 2657 df-un 3039 df-in 3041 df-ss 3048 df-pw 3476 df-sn 3497 df-pr 3498 df-op 3500 |
This theorem is referenced by: opex 4109 otexg 4110 opeliunxp 4552 opbrop 4576 relsnopg 4601 opswapg 4981 elxp4 4982 elxp5 4983 resfunexg 5593 fliftel 5646 fliftel1 5647 oprabid 5755 ovexg 5757 eloprabga 5810 op1st 5996 op2nd 5997 ot1stg 6002 ot2ndg 6003 ot3rdgg 6004 elxp6 6019 mpofvex 6053 algrflem 6078 algrflemg 6079 mpoxopoveq 6089 brtposg 6103 tfr0dm 6171 tfrlemisucaccv 6174 tfrlemibxssdm 6176 tfrlemibfn 6177 tfrlemi14d 6182 tfr1onlemsucaccv 6190 tfr1onlembxssdm 6192 tfr1onlembfn 6193 tfr1onlemres 6198 tfrcllemsucaccv 6203 tfrcllembxssdm 6205 tfrcllembfn 6206 tfrcllemres 6211 fnfi 6775 djulclb 6890 inl11 6900 1stinl 6909 2ndinl 6910 1stinr 6911 2ndinr 6912 mulpipq2 7121 enq0breq 7186 addvalex 7573 peano2nnnn 7582 axcnre 7610 frec2uzrdg 10069 frecuzrdg0 10073 frecuzrdgg 10076 frecuzrdg0t 10082 zfz1isolem1 10470 eucalgval2 11574 crth 11739 phimullem 11740 ennnfonelemp1 11758 setsvala 11827 setsex 11828 setsfun 11831 setsfun0 11832 setsresg 11834 setscom 11836 strslfv 11840 setsslid 11846 strle1g 11886 1strbas 11895 2strbasg 11897 2stropg 11898 2strbas1g 11900 2strop1g 11901 rngbaseg 11912 rngplusgg 11913 rngmulrg 11914 srngbased 11919 srngplusgd 11920 srngmulrd 11921 srnginvld 11922 lmodbased 11930 lmodplusgd 11931 lmodscad 11932 lmodvscad 11933 ipsbased 11938 ipsaddgd 11939 ipsmulrd 11940 ipsscad 11941 ipsvscad 11942 ipsipd 11943 topgrpbasd 11948 topgrpplusgd 11949 topgrptsetd 11950 txlm 12284 |
Copyright terms: Public domain | W3C validator |