![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opexg | GIF version |
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Ref | Expression |
---|---|
opexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfopg 3778 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) | |
2 | elex 2750 | . . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
3 | snexg 4186 | . . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V) | |
4 | 2, 3 | syl 14 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) |
5 | 4 | adantr 276 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V) |
6 | elex 2750 | . . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
7 | prexg 4213 | . . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V) | |
8 | 2, 6, 7 | syl2an 289 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) |
9 | prexg 4213 | . . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V) | |
10 | 5, 8, 9 | syl2anc 411 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V) |
11 | 1, 10 | eqeltrd 2254 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 Vcvv 2739 {csn 3594 {cpr 3595 〈cop 3597 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4123 ax-pow 4176 ax-pr 4211 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2741 df-un 3135 df-in 3137 df-ss 3144 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 |
This theorem is referenced by: opex 4231 otexg 4232 opeliunxp 4683 opbrop 4707 relsnopg 4732 opswapg 5117 elxp4 5118 elxp5 5119 resfunexg 5739 fliftel 5796 fliftel1 5797 oprabid 5909 ovexg 5911 eloprabga 5964 op1st 6149 op2nd 6150 ot1stg 6155 ot2ndg 6156 ot3rdgg 6157 elxp6 6172 mpofvex 6206 algrflem 6232 algrflemg 6233 mpoxopoveq 6243 brtposg 6257 tfr0dm 6325 tfrlemisucaccv 6328 tfrlemibxssdm 6330 tfrlemibfn 6331 tfrlemi14d 6336 tfr1onlemsucaccv 6344 tfr1onlembxssdm 6346 tfr1onlembfn 6347 tfr1onlemres 6352 tfrcllemsucaccv 6357 tfrcllembxssdm 6359 tfrcllembfn 6360 tfrcllemres 6365 fnfi 6938 djulclb 7056 inl11 7066 1stinl 7075 2ndinl 7076 1stinr 7077 2ndinr 7078 mulpipq2 7372 enq0breq 7437 addvalex 7845 peano2nnnn 7854 axcnre 7882 frec2uzrdg 10411 frecuzrdg0 10415 frecuzrdgg 10418 frecuzrdg0t 10424 zfz1isolem1 10822 eucalgval2 12055 crth 12226 phimullem 12227 ennnfonelemp1 12409 setsvala 12495 setsex 12496 setsfun 12499 setsfun0 12500 setsresg 12502 setscom 12504 strslfv 12509 setsslid 12515 strle1g 12567 1strbas 12578 2strbasg 12580 2stropg 12581 2strbas1g 12583 2strop1g 12584 rngbaseg 12596 rngplusgg 12597 rngmulrg 12598 srngbased 12607 srngplusgd 12608 srngmulrd 12609 srnginvld 12610 lmodbased 12625 lmodplusgd 12626 lmodscad 12627 lmodvscad 12628 ipsbased 12637 ipsaddgd 12638 ipsmulrd 12639 ipsscad 12640 ipsvscad 12641 ipsipd 12642 topgrpbasd 12657 topgrpplusgd 12658 topgrptsetd 12659 prdsex 12723 imasex 12731 imasival 12732 imasbas 12733 imasplusg 12734 imasmulr 12735 imasaddfnlemg 12740 imasaddvallemg 12741 xpsfval 12772 xpsval 12776 intopsn 12791 mgm1 12794 sgrp1 12821 mnd1 12852 mnd1id 12853 grp1 12981 grp1inv 12982 ring1 13241 txlm 13864 |
Copyright terms: Public domain | W3C validator |