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

Theorem xpex 7004
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 7002 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
41, 2, 3mp2an 708 1 (𝐴 × 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231   × cxp 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-opab 4746  df-xp 5149  df-rel 5150
This theorem is referenced by:  oprabex  7198  oprabex3  7199  fnpm  7907  mapsnf1o2  7947  ixpsnf1o  7990  xpsnen  8085  endisj  8088  xpcomen  8092  xpassen  8095  xpmapenlem  8168  mapunen  8170  unxpdomlem3  8207  hartogslem1  8488  rankxpl  8776  rankfu  8778  rankmapu  8779  rankxplim  8780  rankxplim2  8781  rankxplim3  8782  rankxpsuc  8783  r0weon  8873  infxpenlem  8874  infxpenc2lem2  8881  dfac3  8982  dfac5lem2  8985  dfac5lem3  8986  dfac5lem4  8987  cdafn  9029  unctb  9065  axcc2lem  9296  axdc3lem  9310  axdc4lem  9315  enqex  9782  nqex  9783  enrex  9926  axcnex  10006  zexALT  11434  cnexALT  11866  addex  11868  mulex  11869  ixxex  12224  shftfval  13854  climconst2  14323  cpnnen  15002  ruclem13  15015  cnso  15020  prdsval  16162  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdsle  16169  prdsds  16171  prdshom  16174  prdsco  16175  fnmrc  16314  mrcfval  16315  mreacs  16366  comfffval  16405  oppccofval  16423  sectfval  16458  brssc  16521  sscpwex  16522  isssc  16527  isfunc  16571  isfuncd  16572  idfu2nd  16584  idfu1st  16586  idfucl  16588  wunfunc  16606  fuccofval  16666  homafval  16726  homaf  16727  homaval  16728  coapm  16768  catccofval  16797  catcfuccl  16806  xpcval  16864  xpcbas  16865  xpchom  16867  xpccofval  16869  1stfval  16878  2ndfval  16881  1stfcl  16884  2ndfcl  16885  catcxpccl  16894  evlf2  16905  evlf1  16907  evlfcl  16909  hof1fval  16940  hof2fval  16942  hofcl  16946  ipoval  17201  letsr  17274  plusffval  17294  frmdplusg  17438  eqgfval  17689  efglem  18175  efgval  18176  scaffval  18929  psrplusg  19429  ltbval  19519  opsrle  19523  evlslem2  19560  evlssca  19570  mpfind  19584  evls1sca  19736  pf1ind  19767  cnfldds  19804  cnfldfun  19806  cnfldfunALT  19807  xrsadd  19811  xrsmul  19812  xrsle  19814  xrsds  19837  znle  19932  ipffval  20041  pjfval  20098  mat1dimmul  20330  2ndcctbss  21306  txuni2  21416  txbas  21418  eltx  21419  txcnp  21471  txcnmpt  21475  txrest  21482  txlm  21499  tx1stc  21501  tx2ndc  21502  txkgen  21503  txflf  21857  cnextfval  21913  distgp  21950  indistgp  21951  ustfn  22052  ustn0  22071  ussid  22111  ressuss  22114  ishtpy  22818  isphtpc  22840  elovolm  23289  elovolmr  23290  ovolmge0  23291  ovolgelb  23294  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovolshftlem2  23324  ovolicc2  23336  ioombl1  23376  dyadmbl  23414  vitali  23427  mbfimaopnlem  23467  dvfval  23706  plyeq0lem  24011  taylfval  24158  ulmval  24179  dmarea  24729  dchrplusg  25017  iscgrg  25452  ishlg  25542  ishpg  25696  iscgra  25746  isinag  25774  axlowdimlem15  25881  axlowdim  25886  isgrpoi  27480  sspval  27706  0ofval  27770  ajfval  27792  hvmulex  27996  inftmrel  29862  isinftm  29863  smatrcl  29990  tpr2rico  30086  faeval  30437  mbfmco2  30455  br2base  30459  sxbrsigalem0  30461  sxbrsigalem3  30462  dya2iocrfn  30469  dya2iocct  30470  dya2iocnrect  30471  dya2iocuni  30473  dya2iocucvr  30474  sxbrsigalem2  30476  eulerpartlemgs2  30570  ccatmulgnn0dir  30747  afsval  30877  cvmlift2lem9  31419  mexval  31525  mdvval  31527  mpstval  31558  brimg  32169  brrestrict  32181  colinearex  32292  poimirlem4  33543  poimirlem28  33567  mblfinlem1  33576  heiborlem3  33742  rrnval  33756  ismrer1  33767  dfcnvrefrels2  34416  dfcnvrefrels3  34417  lcvfbr  34625  cmtfvalN  34815  cvrfval  34873  dvhvbase  36693  dvhfvadd  36697  dvhfvsca  36706  dibval  36748  dibfna  36760  dicval  36782  hdmap1fval  37403  mzpincl  37614  pellexlem3  37712  pellexlem4  37713  pellexlem5  37714  aomclem6  37946  trclexi  38244  rtrclexi  38245  brtrclfv2  38336  hoiprodcl2  41090  hoicvrrex  41091  ovn0lem  41100  ovnhoilem1  41136  ovnlecvr2  41145  opnvonmbllem1  41167  opnvonmbllem2  41168  ovolval2lem  41178  ovolval2  41179  ovolval3  41182  ovolval4lem2  41185  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  smflimlem6  41305  elpglem3  42784  aacllem  42875
  Copyright terms: Public domain W3C validator