MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpex Structured version   Visualization version   GIF version

Theorem xpex 7475
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
Hypotheses
Ref Expression
xpex.1 𝐴 ∈ V
xpex.2 𝐵 ∈ V
Assertion
Ref Expression
xpex (𝐴 × 𝐵) ∈ V

Proof of Theorem xpex
StepHypRef Expression
1 xpex.1 . 2 𝐴 ∈ V
2 xpex.2 . 2 𝐵 ∈ V
3 xpexg 7472 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
41, 2, 3mp2an 690 1 (𝐴 × 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2110  Vcvv 3494   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-opab 5128  df-xp 5560  df-rel 5561
This theorem is referenced by:  oprabex  7676  oprabex3  7677  mpoexw  7775  fnpm  8413  mapsnf1o2  8457  ixpsnf1o  8501  xpsnen  8600  endisj  8603  xpcomen  8607  xpassen  8610  xpmapenlem  8683  mapunen  8685  unxpdomlem3  8723  hartogslem1  9005  rankxpl  9303  rankfu  9305  rankmapu  9306  rankxplim  9307  rankxplim2  9308  rankxplim3  9309  rankxpsuc  9310  r0weon  9437  infxpenlem  9438  infxpenc2lem2  9445  dfac3  9546  dfac5lem2  9549  dfac5lem3  9550  dfac5lem4  9551  unctb  9626  axcc2lem  9857  axdc3lem  9871  axdc4lem  9876  enqex  10343  nqex  10344  nrex1  10485  enrex  10488  axcnex  10568  zexALT  12000  cnexALT  12384  addex  12386  mulex  12387  ixxex  12748  shftfval  14428  climconst2  14904  cpnnen  15581  ruclem13  15594  cnso  15599  prdsval  16727  prdsplusg  16730  prdsmulr  16731  prdsvsca  16732  prdsle  16734  prdsds  16736  prdshom  16739  prdsco  16740  fnmrc  16877  mrcfval  16878  mreacs  16928  comfffval  16967  oppccofval  16985  sectfval  17020  brssc  17083  sscpwex  17084  isssc  17089  isfunc  17133  isfuncd  17134  idfu2nd  17146  idfu1st  17148  idfucl  17150  wunfunc  17168  fuccofval  17228  homafval  17288  homaf  17289  homaval  17290  coapm  17330  catccofval  17359  catcfuccl  17368  xpcval  17426  xpcbas  17427  xpchom  17429  xpccofval  17431  1stfval  17440  2ndfval  17443  1stfcl  17446  2ndfcl  17447  catcxpccl  17456  evlf2  17467  evlf1  17469  evlfcl  17471  hof1fval  17502  hof2fval  17504  hofcl  17508  ipoval  17763  letsr  17836  frmdplusg  18018  eqgfval  18327  efglem  18841  efgval  18842  psrplusg  20160  ltbval  20251  opsrle  20255  evlslem2  20291  evlssca  20301  mpfind  20319  evls1sca  20485  pf1ind  20517  cnfldds  20554  cnfldfun  20556  cnfldfunALT  20557  xrsadd  20561  xrsmul  20562  xrsle  20564  xrsds  20587  znle  20682  pjfval  20849  mat1dimmul  21084  2ndcctbss  22062  txuni2  22172  txbas  22174  eltx  22175  txcnp  22227  txcnmpt  22231  txrest  22238  txlm  22255  tx1stc  22257  tx2ndc  22258  txkgen  22259  txflf  22613  cnextfval  22669  distgp  22706  indistgp  22707  ustfn  22809  ustn0  22828  ussid  22868  ressuss  22871  ishtpy  23575  isphtpc  23597  elovolmlem  24074  dyadmbl  24200  vitali  24213  mbfimaopnlem  24255  dvfval  24494  plyeq0lem  24799  taylfval  24946  ulmval  24967  dmarea  25534  dchrplusg  25822  tgjustc1  26260  tgjustc2  26261  iscgrg  26297  ishlg  26387  ishpg  26544  iscgra  26594  isinag  26623  isleag  26632  axlowdimlem15  26741  axlowdim  26746  isgrpoi  28274  sspval  28499  0ofval  28563  ajfval  28585  hvmulex  28787  inftmrel  30809  isinftm  30810  smatrcl  31061  tpr2rico  31155  faeval  31505  mbfmco2  31523  br2base  31527  sxbrsigalem0  31529  sxbrsigalem3  31530  dya2iocrfn  31537  dya2iocct  31538  dya2iocnrect  31539  dya2iocuni  31541  dya2iocucvr  31542  sxbrsigalem2  31544  eulerpartlemgs2  31638  ccatmulgnn0dir  31812  afsval  31942  cvmlift2lem9  32558  satfv0  32605  satf00  32621  prv1n  32678  mexval  32749  mdvval  32751  mpstval  32782  brimg  33398  brrestrict  33410  colinearex  33521  poimirlem4  34895  poimirlem28  34919  mblfinlem1  34928  heiborlem3  35090  rrnval  35104  ismrer1  35115  dfcnvrefrels2  35765  dfcnvrefrels3  35766  lcvfbr  36155  cmtfvalN  36345  cvrfval  36403  dvhvbase  38222  dvhfvadd  38226  dvhfvsca  38235  dibval  38277  dibfna  38289  dicval  38311  hdmap1fval  38931  mzpincl  39331  pellexlem3  39428  pellexlem4  39429  pellexlem5  39430  aomclem6  39659  trclexi  39980  rtrclexi  39981  brtrclfv2  40072  hoiprodcl2  42838  hoicvrrex  42839  ovn0lem  42848  ovnhoilem1  42884  ovnlecvr2  42893  opnvonmbllem1  42915  opnvonmbllem2  42916  ovolval2lem  42926  ovolval2  42927  ovolval3  42930  ovolval4lem2  42933  ovolval5lem2  42936  ovnovollem1  42939  ovnovollem2  42940  smflimlem6  43053  elpglem3  44816  aacllem  44903
  Copyright terms: Public domain W3C validator