![]() |
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 7220 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V) | |
4 | 1, 2, 3 | mp2an 685 | 1 ⊢ (𝐴 × 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 Vcvv 3414 × cxp 5340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pow 5065 ax-pr 5127 ax-un 7209 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-opab 4936 df-xp 5348 df-rel 5349 |
This theorem is referenced by: oprabex 7416 oprabex3 7417 fnpm 8130 mapsnf1o2 8172 ixpsnf1o 8215 xpsnen 8313 endisj 8316 xpcomen 8320 xpassen 8323 xpmapenlem 8396 mapunen 8398 unxpdomlem3 8435 hartogslem1 8716 rankxpl 9015 rankfu 9017 rankmapu 9018 rankxplim 9019 rankxplim2 9020 rankxplim3 9021 rankxpsuc 9022 r0weon 9148 infxpenlem 9149 infxpenc2lem2 9156 dfac3 9257 dfac5lem2 9260 dfac5lem3 9261 dfac5lem4 9262 cdafn 9306 unctb 9342 axcc2lem 9573 axdc3lem 9587 axdc4lem 9592 enqex 10059 nqex 10060 nrex1 10201 enrex 10204 axcnex 10284 zexALT 11723 cnexALT 12108 addex 12110 mulex 12111 ixxex 12474 shftfval 14187 climconst2 14656 cpnnen 15332 ruclem13 15345 cnso 15350 prdsval 16468 prdsplusg 16471 prdsmulr 16472 prdsvsca 16473 prdsle 16475 prdsds 16477 prdshom 16480 prdsco 16481 fnmrc 16620 mrcfval 16621 mreacs 16671 comfffval 16710 oppccofval 16728 sectfval 16763 brssc 16826 sscpwex 16827 isssc 16832 isfunc 16876 isfuncd 16877 idfu2nd 16889 idfu1st 16891 idfucl 16893 wunfunc 16911 fuccofval 16971 homafval 17031 homaf 17032 homaval 17033 coapm 17073 catccofval 17102 catcfuccl 17111 xpcval 17170 xpcbas 17171 xpchom 17173 xpccofval 17175 1stfval 17184 2ndfval 17187 1stfcl 17190 2ndfcl 17191 catcxpccl 17200 evlf2 17211 evlf1 17213 evlfcl 17215 hof1fval 17246 hof2fval 17248 hofcl 17252 ipoval 17507 letsr 17580 plusffval 17600 frmdplusg 17745 eqgfval 17993 efglem 18480 efgval 18481 scaffval 19237 psrplusg 19742 ltbval 19832 opsrle 19836 evlslem2 19872 evlssca 19882 mpfind 19896 evls1sca 20048 pf1ind 20079 cnfldds 20116 cnfldfun 20118 cnfldfunALT 20119 xrsadd 20123 xrsmul 20124 xrsle 20126 xrsds 20149 znle 20244 ipffval 20355 pjfval 20413 mat1dimmul 20650 2ndcctbss 21629 txuni2 21739 txbas 21741 eltx 21742 txcnp 21794 txcnmpt 21798 txrest 21805 txlm 21822 tx1stc 21824 tx2ndc 21825 txkgen 21826 txflf 22180 cnextfval 22236 distgp 22273 indistgp 22274 ustfn 22375 ustn0 22394 ussid 22434 ressuss 22437 ishtpy 23141 isphtpc 23163 elovolmlem 23640 dyadmbl 23766 vitali 23779 mbfimaopnlem 23821 dvfval 24060 plyeq0lem 24365 taylfval 24512 ulmval 24533 dmarea 25097 dchrplusg 25385 tgjustc1 25787 tgjustc2 25788 iscgrg 25824 ishlg 25914 ishpg 26068 iscgra 26118 isinag 26147 axlowdimlem15 26255 axlowdim 26260 isgrpoi 27908 sspval 28133 0ofval 28197 ajfval 28219 hvmulex 28423 inftmrel 30279 isinftm 30280 smatrcl 30407 tpr2rico 30503 faeval 30854 mbfmco2 30872 br2base 30876 sxbrsigalem0 30878 sxbrsigalem3 30879 dya2iocrfn 30886 dya2iocct 30887 dya2iocnrect 30888 dya2iocuni 30890 dya2iocucvr 30891 sxbrsigalem2 30893 eulerpartlemgs2 30987 ccatmulgnn0dir 31166 afsval 31298 cvmlift2lem9 31839 mexval 31945 mdvval 31947 mpstval 31978 brimg 32583 brrestrict 32595 colinearex 32706 cnfinltrel 33786 poimirlem4 33957 poimirlem28 33981 mblfinlem1 33990 heiborlem3 34154 rrnval 34168 ismrer1 34179 dfcnvrefrels2 34824 dfcnvrefrels3 34825 lcvfbr 35095 cmtfvalN 35285 cvrfval 35343 dvhvbase 37162 dvhfvadd 37166 dvhfvsca 37175 dibval 37217 dibfna 37229 dicval 37251 hdmap1fval 37871 mzpincl 38141 pellexlem3 38239 pellexlem4 38240 pellexlem5 38241 aomclem6 38472 trclexi 38768 rtrclexi 38769 brtrclfv2 38860 hoiprodcl2 41563 hoicvrrex 41564 ovn0lem 41573 ovnhoilem1 41609 ovnlecvr2 41618 opnvonmbllem1 41640 opnvonmbllem2 41641 ovolval2lem 41651 ovolval2 41652 ovolval3 41655 ovolval4lem2 41658 ovolval5lem2 41661 ovnovollem1 41664 ovnovollem2 41665 smflimlem6 41778 elpglem3 43354 aacllem 43443 |
Copyright terms: Public domain | W3C validator |