![]() |
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 3791 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2763 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | snexg 4202 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 14 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | adantr 276 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | elex 2763 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | prexg 4229 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 2, 6, 7 | syl2an 289 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | prexg 4229 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 5, 8, 9 | syl2anc 411 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 1, 10 | eqeltrd 2266 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4192 ax-pr 4227 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 |
This theorem is referenced by: opex 4247 otexg 4248 opeliunxp 4699 opbrop 4723 relsnopg 4748 opswapg 5133 elxp4 5134 elxp5 5135 resfunexg 5758 fliftel 5815 fliftel1 5816 oprabid 5928 ovexg 5930 eloprabga 5983 op1st 6171 op2nd 6172 ot1stg 6177 ot2ndg 6178 ot3rdgg 6179 elxp6 6194 mpofvex 6228 algrflem 6254 algrflemg 6255 mpoxopoveq 6265 brtposg 6279 tfr0dm 6347 tfrlemisucaccv 6350 tfrlemibxssdm 6352 tfrlemibfn 6353 tfrlemi14d 6358 tfr1onlemsucaccv 6366 tfr1onlembxssdm 6368 tfr1onlembfn 6369 tfr1onlemres 6374 tfrcllemsucaccv 6379 tfrcllembxssdm 6381 tfrcllembfn 6382 tfrcllemres 6387 fnfi 6966 djulclb 7084 inl11 7094 1stinl 7103 2ndinl 7104 1stinr 7105 2ndinr 7106 mulpipq2 7400 enq0breq 7465 addvalex 7873 peano2nnnn 7882 axcnre 7910 frec2uzrdg 10440 frecuzrdg0 10444 frecuzrdgg 10447 frecuzrdg0t 10453 zfz1isolem1 10852 eucalgval2 12085 crth 12256 phimullem 12257 ennnfonelemp1 12457 setsvala 12543 setsex 12544 setsfun 12547 setsfun0 12548 setsresg 12550 setscom 12552 strslfv 12557 setsslid 12563 strle1g 12618 1strbas 12629 2strbasg 12631 2stropg 12632 2strbas1g 12634 2strop1g 12635 rngbaseg 12647 rngplusgg 12648 rngmulrg 12649 srngbased 12658 srngplusgd 12659 srngmulrd 12660 srnginvld 12661 lmodbased 12676 lmodplusgd 12677 lmodscad 12678 lmodvscad 12679 ipsbased 12688 ipsaddgd 12689 ipsmulrd 12690 ipsscad 12691 ipsvscad 12692 ipsipd 12693 topgrpbasd 12708 topgrpplusgd 12709 topgrptsetd 12710 prdsex 12774 imasex 12782 imasival 12783 imasbas 12784 imasplusg 12785 imasmulr 12786 imasaddfnlemg 12791 imasaddvallemg 12792 xpsfval 12824 xpsval 12828 intopsn 12843 mgm1 12846 sgrp1 12874 mnd1 12907 mnd1id 12908 grp1 13050 grp1inv 13051 ring1 13411 psrval 13944 fnpsr 13945 psrbasg 13951 psrplusgg 13954 txlm 14239 |
Copyright terms: Public domain | W3C validator |