Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpex | Structured version Visualization version GIF version |
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpex.1 | ⊢ 𝐴 ∈ V |
xpex.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
xpex | ⊢ (𝐴 × 𝐵) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | xpex.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | xpexg 7462 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴 × 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3492 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-opab 5120 df-xp 5554 df-rel 5555 |
This theorem is referenced by: oprabex 7666 oprabex3 7667 mpoexw 7765 fnpm 8403 mapsnf1o2 8446 ixpsnf1o 8490 xpsnen 8589 endisj 8592 xpcomen 8596 xpassen 8599 xpmapenlem 8672 mapunen 8674 unxpdomlem3 8712 hartogslem1 8994 rankxpl 9292 rankfu 9294 rankmapu 9295 rankxplim 9296 rankxplim2 9297 rankxplim3 9298 rankxpsuc 9299 r0weon 9426 infxpenlem 9427 infxpenc2lem2 9434 dfac3 9535 dfac5lem2 9538 dfac5lem3 9539 dfac5lem4 9540 unctb 9615 axcc2lem 9846 axdc3lem 9860 axdc4lem 9865 enqex 10332 nqex 10333 nrex1 10474 enrex 10477 axcnex 10557 zexALT 11989 cnexALT 12373 addex 12375 mulex 12376 ixxex 12737 shftfval 14417 climconst2 14893 cpnnen 15570 ruclem13 15583 cnso 15588 prdsval 16716 prdsplusg 16719 prdsmulr 16720 prdsvsca 16721 prdsle 16723 prdsds 16725 prdshom 16728 prdsco 16729 fnmrc 16866 mrcfval 16867 mreacs 16917 comfffval 16956 oppccofval 16974 sectfval 17009 brssc 17072 sscpwex 17073 isssc 17078 isfunc 17122 isfuncd 17123 idfu2nd 17135 idfu1st 17137 idfucl 17139 wunfunc 17157 fuccofval 17217 homafval 17277 homaf 17278 homaval 17279 coapm 17319 catccofval 17348 catcfuccl 17357 xpcval 17415 xpcbas 17416 xpchom 17418 xpccofval 17420 1stfval 17429 2ndfval 17432 1stfcl 17435 2ndfcl 17436 catcxpccl 17445 evlf2 17456 evlf1 17458 evlfcl 17460 hof1fval 17491 hof2fval 17493 hofcl 17497 ipoval 17752 letsr 17825 frmdplusg 18007 eqgfval 18266 efglem 18771 efgval 18772 psrplusg 20089 ltbval 20180 opsrle 20184 evlslem2 20220 evlssca 20230 mpfind 20248 evls1sca 20414 pf1ind 20446 cnfldds 20483 cnfldfun 20485 cnfldfunALT 20486 xrsadd 20490 xrsmul 20491 xrsle 20493 xrsds 20516 znle 20611 pjfval 20778 mat1dimmul 21013 2ndcctbss 21991 txuni2 22101 txbas 22103 eltx 22104 txcnp 22156 txcnmpt 22160 txrest 22167 txlm 22184 tx1stc 22186 tx2ndc 22187 txkgen 22188 txflf 22542 cnextfval 22598 distgp 22635 indistgp 22636 ustfn 22737 ustn0 22756 ussid 22796 ressuss 22799 ishtpy 23503 isphtpc 23525 elovolmlem 24002 dyadmbl 24128 vitali 24141 mbfimaopnlem 24183 dvfval 24422 plyeq0lem 24727 taylfval 24874 ulmval 24895 dmarea 25462 dchrplusg 25750 tgjustc1 26188 tgjustc2 26189 iscgrg 26225 ishlg 26315 ishpg 26472 iscgra 26522 isinag 26551 isleag 26560 axlowdimlem15 26669 axlowdim 26674 isgrpoi 28202 sspval 28427 0ofval 28491 ajfval 28513 hvmulex 28715 inftmrel 30736 isinftm 30737 smatrcl 30960 tpr2rico 31054 faeval 31404 mbfmco2 31422 br2base 31426 sxbrsigalem0 31428 sxbrsigalem3 31429 dya2iocrfn 31436 dya2iocct 31437 dya2iocnrect 31438 dya2iocuni 31440 dya2iocucvr 31441 sxbrsigalem2 31443 eulerpartlemgs2 31537 ccatmulgnn0dir 31711 afsval 31841 cvmlift2lem9 32455 satfv0 32502 satf00 32518 prv1n 32575 mexval 32646 mdvval 32648 mpstval 32679 brimg 33295 brrestrict 33307 colinearex 33418 poimirlem4 34777 poimirlem28 34801 mblfinlem1 34810 heiborlem3 34972 rrnval 34986 ismrer1 34997 dfcnvrefrels2 35646 dfcnvrefrels3 35647 lcvfbr 36036 cmtfvalN 36226 cvrfval 36284 dvhvbase 38103 dvhfvadd 38107 dvhfvsca 38116 dibval 38158 dibfna 38170 dicval 38192 hdmap1fval 38812 mzpincl 39209 pellexlem3 39306 pellexlem4 39307 pellexlem5 39308 aomclem6 39537 trclexi 39858 rtrclexi 39859 brtrclfv2 39950 hoiprodcl2 42714 hoicvrrex 42715 ovn0lem 42724 ovnhoilem1 42760 ovnlecvr2 42769 opnvonmbllem1 42791 opnvonmbllem2 42792 ovolval2lem 42802 ovolval2 42803 ovolval3 42806 ovolval4lem2 42809 ovolval5lem2 42812 ovnovollem1 42815 ovnovollem2 42816 smflimlem6 42929 elpglem3 44743 aacllem 44830 |
Copyright terms: Public domain | W3C validator |