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

Theorem xpex 7115
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 7113 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
41, 2, 3mp2an 710 1 (𝐴 × 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2127  Vcvv 3328   × cxp 5252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-opab 4853  df-xp 5260  df-rel 5261
This theorem is referenced by:  oprabex  7309  oprabex3  7310  fnpm  8019  mapsnf1o2  8059  ixpsnf1o  8102  xpsnen  8197  endisj  8200  xpcomen  8204  xpassen  8207  xpmapenlem  8280  mapunen  8282  unxpdomlem3  8319  hartogslem1  8600  rankxpl  8899  rankfu  8901  rankmapu  8902  rankxplim  8903  rankxplim2  8904  rankxplim3  8905  rankxpsuc  8906  r0weon  8996  infxpenlem  8997  infxpenc2lem2  9004  dfac3  9105  dfac5lem2  9108  dfac5lem3  9109  dfac5lem4  9110  cdafn  9154  unctb  9190  axcc2lem  9421  axdc3lem  9435  axdc4lem  9440  enqex  9907  nqex  9908  enrex  10051  axcnex  10131  zexALT  11559  cnexALT  11992  addex  11994  mulex  11995  ixxex  12350  shftfval  13980  climconst2  14449  cpnnen  15128  ruclem13  15141  cnso  15146  prdsval  16288  prdsplusg  16291  prdsmulr  16292  prdsvsca  16293  prdsle  16295  prdsds  16297  prdshom  16300  prdsco  16301  fnmrc  16440  mrcfval  16441  mreacs  16491  comfffval  16530  oppccofval  16548  sectfval  16583  brssc  16646  sscpwex  16647  isssc  16652  isfunc  16696  isfuncd  16697  idfu2nd  16709  idfu1st  16711  idfucl  16713  wunfunc  16731  fuccofval  16791  homafval  16851  homaf  16852  homaval  16853  coapm  16893  catccofval  16922  catcfuccl  16931  xpcval  16989  xpcbas  16990  xpchom  16992  xpccofval  16994  1stfval  17003  2ndfval  17006  1stfcl  17009  2ndfcl  17010  catcxpccl  17019  evlf2  17030  evlf1  17032  evlfcl  17034  hof1fval  17065  hof2fval  17067  hofcl  17071  ipoval  17326  letsr  17399  plusffval  17419  frmdplusg  17563  eqgfval  17814  efglem  18300  efgval  18301  scaffval  19054  psrplusg  19554  ltbval  19644  opsrle  19648  evlslem2  19685  evlssca  19695  mpfind  19709  evls1sca  19861  pf1ind  19892  cnfldds  19929  cnfldfun  19931  cnfldfunALT  19932  xrsadd  19936  xrsmul  19937  xrsle  19939  xrsds  19962  znle  20057  ipffval  20166  pjfval  20223  mat1dimmul  20455  2ndcctbss  21431  txuni2  21541  txbas  21543  eltx  21544  txcnp  21596  txcnmpt  21600  txrest  21607  txlm  21624  tx1stc  21626  tx2ndc  21627  txkgen  21628  txflf  21982  cnextfval  22038  distgp  22075  indistgp  22076  ustfn  22177  ustn0  22196  ussid  22236  ressuss  22239  ishtpy  22943  isphtpc  22965  elovolm  23414  elovolmr  23415  ovolmge0  23416  ovolgelb  23419  ovolunlem1a  23435  ovolunlem1  23436  ovoliunlem1  23441  ovoliunlem2  23442  ovolshftlem2  23449  ovolicc2  23461  ioombl1  23501  dyadmbl  23539  vitali  23552  mbfimaopnlem  23592  dvfval  23831  plyeq0lem  24136  taylfval  24283  ulmval  24304  dmarea  24854  dchrplusg  25142  iscgrg  25577  ishlg  25667  ishpg  25821  iscgra  25871  isinag  25899  axlowdimlem15  26006  axlowdim  26011  isgrpoi  27632  sspval  27858  0ofval  27922  ajfval  27944  hvmulex  28148  inftmrel  30014  isinftm  30015  smatrcl  30142  tpr2rico  30238  faeval  30589  mbfmco2  30607  br2base  30611  sxbrsigalem0  30613  sxbrsigalem3  30614  dya2iocrfn  30621  dya2iocct  30622  dya2iocnrect  30623  dya2iocuni  30625  dya2iocucvr  30626  sxbrsigalem2  30628  eulerpartlemgs2  30722  ccatmulgnn0dir  30899  afsval  31029  cvmlift2lem9  31571  mexval  31677  mdvval  31679  mpstval  31710  brimg  32321  brrestrict  32333  colinearex  32444  poimirlem4  33695  poimirlem28  33719  mblfinlem1  33728  heiborlem3  33894  rrnval  33908  ismrer1  33919  dfcnvrefrels2  34568  dfcnvrefrels3  34569  lcvfbr  34779  cmtfvalN  34969  cvrfval  35027  dvhvbase  36847  dvhfvadd  36851  dvhfvsca  36860  dibval  36902  dibfna  36914  dicval  36936  hdmap1fval  37557  mzpincl  37768  pellexlem3  37866  pellexlem4  37867  pellexlem5  37868  aomclem6  38100  trclexi  38398  rtrclexi  38399  brtrclfv2  38490  hoiprodcl2  41244  hoicvrrex  41245  ovn0lem  41254  ovnhoilem1  41290  ovnlecvr2  41299  opnvonmbllem1  41321  opnvonmbllem2  41322  ovolval2lem  41332  ovolval2  41333  ovolval3  41336  ovolval4lem2  41339  ovolval5lem2  41342  ovnovollem1  41345  ovnovollem2  41346  smflimlem6  41459  elpglem3  42938  aacllem  43029
  Copyright terms: Public domain W3C validator