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 7461 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴 × 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3495 × cxp 5547 |
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 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-opab 5121 df-xp 5555 df-rel 5556 |
This theorem is referenced by: oprabex 7668 oprabex3 7669 mpoexw 7767 fnpm 8404 mapsnf1o2 8447 ixpsnf1o 8491 xpsnen 8590 endisj 8593 xpcomen 8597 xpassen 8600 xpmapenlem 8673 mapunen 8675 unxpdomlem3 8713 hartogslem1 8995 rankxpl 9293 rankfu 9295 rankmapu 9296 rankxplim 9297 rankxplim2 9298 rankxplim3 9299 rankxpsuc 9300 r0weon 9427 infxpenlem 9428 infxpenc2lem2 9435 dfac3 9536 dfac5lem2 9539 dfac5lem3 9540 dfac5lem4 9541 unctb 9616 axcc2lem 9847 axdc3lem 9861 axdc4lem 9866 enqex 10333 nqex 10334 nrex1 10475 enrex 10478 axcnex 10558 zexALT 11990 cnexALT 12375 addex 12377 mulex 12378 ixxex 12739 shftfval 14419 climconst2 14895 cpnnen 15572 ruclem13 15585 cnso 15590 prdsval 16718 prdsplusg 16721 prdsmulr 16722 prdsvsca 16723 prdsle 16725 prdsds 16727 prdshom 16730 prdsco 16731 fnmrc 16868 mrcfval 16869 mreacs 16919 comfffval 16958 oppccofval 16976 sectfval 17011 brssc 17074 sscpwex 17075 isssc 17080 isfunc 17124 isfuncd 17125 idfu2nd 17137 idfu1st 17139 idfucl 17141 wunfunc 17159 fuccofval 17219 homafval 17279 homaf 17280 homaval 17281 coapm 17321 catccofval 17350 catcfuccl 17359 xpcval 17417 xpcbas 17418 xpchom 17420 xpccofval 17422 1stfval 17431 2ndfval 17434 1stfcl 17437 2ndfcl 17438 catcxpccl 17447 evlf2 17458 evlf1 17460 evlfcl 17462 hof1fval 17493 hof2fval 17495 hofcl 17499 ipoval 17754 letsr 17827 frmdplusg 18009 eqgfval 18268 efglem 18773 efgval 18774 psrplusg 20091 ltbval 20182 opsrle 20186 evlslem2 20222 evlssca 20232 mpfind 20250 evls1sca 20416 pf1ind 20448 cnfldds 20485 cnfldfun 20487 cnfldfunALT 20488 xrsadd 20492 xrsmul 20493 xrsle 20495 xrsds 20518 znle 20613 pjfval 20780 mat1dimmul 21015 2ndcctbss 21993 txuni2 22103 txbas 22105 eltx 22106 txcnp 22158 txcnmpt 22162 txrest 22169 txlm 22186 tx1stc 22188 tx2ndc 22189 txkgen 22190 txflf 22544 cnextfval 22600 distgp 22637 indistgp 22638 ustfn 22739 ustn0 22758 ussid 22798 ressuss 22801 ishtpy 23505 isphtpc 23527 elovolmlem 24004 dyadmbl 24130 vitali 24143 mbfimaopnlem 24185 dvfval 24424 plyeq0lem 24729 taylfval 24876 ulmval 24897 dmarea 25463 dchrplusg 25751 tgjustc1 26189 tgjustc2 26190 iscgrg 26226 ishlg 26316 ishpg 26473 iscgra 26523 isinag 26552 isleag 26561 axlowdimlem15 26670 axlowdim 26675 isgrpoi 28203 sspval 28428 0ofval 28492 ajfval 28514 hvmulex 28716 inftmrel 30737 isinftm 30738 smatrcl 30961 tpr2rico 31055 faeval 31405 mbfmco2 31423 br2base 31427 sxbrsigalem0 31429 sxbrsigalem3 31430 dya2iocrfn 31437 dya2iocct 31438 dya2iocnrect 31439 dya2iocuni 31441 dya2iocucvr 31442 sxbrsigalem2 31444 eulerpartlemgs2 31538 ccatmulgnn0dir 31712 afsval 31842 cvmlift2lem9 32456 satfv0 32503 satf00 32519 prv1n 32576 mexval 32647 mdvval 32649 mpstval 32680 brimg 33296 brrestrict 33308 colinearex 33419 poimirlem4 34778 poimirlem28 34802 mblfinlem1 34811 heiborlem3 34974 rrnval 34988 ismrer1 34999 dfcnvrefrels2 35648 dfcnvrefrels3 35649 lcvfbr 36038 cmtfvalN 36228 cvrfval 36286 dvhvbase 38105 dvhfvadd 38109 dvhfvsca 38118 dibval 38160 dibfna 38172 dicval 38194 hdmap1fval 38814 mzpincl 39211 pellexlem3 39308 pellexlem4 39309 pellexlem5 39310 aomclem6 39539 trclexi 39860 rtrclexi 39861 brtrclfv2 39952 hoiprodcl2 42718 hoicvrrex 42719 ovn0lem 42728 ovnhoilem1 42764 ovnlecvr2 42773 opnvonmbllem1 42795 opnvonmbllem2 42796 ovolval2lem 42806 ovolval2 42807 ovolval3 42810 ovolval4lem2 42813 ovolval5lem2 42816 ovnovollem1 42819 ovnovollem2 42820 smflimlem6 42933 elpglem3 44713 aacllem 44800 |
Copyright terms: Public domain | W3C validator |