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

Theorem xpex 4904
Description: The cross 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  |-  A  e. 
_V
xpex.2  |-  B  e. 
_V
Assertion
Ref Expression
xpex  |-  ( A  X.  B )  e. 
_V

Proof of Theorem xpex
StepHypRef Expression
1 xpex.1 . 2  |-  A  e. 
_V
2 xpex.2 . 2  |-  B  e. 
_V
3 xpexg 4903 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 653 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1715   _Vcvv 2873    X. cxp 4790
This theorem is referenced by:  oprabex  6087  oprabex3  6088  fnpm  6923  mapsnf1o2  6958  ixpsnf1o  6999  xpsnen  7089  endisj  7092  xpcomen  7096  xpassen  7099  xpmapenlem  7171  mapunen  7173  unxpdomlem3  7212  hartogslem1  7404  rankxpl  7694  rankxplim  7696  rankxplim2  7697  rankxplim3  7698  rankxpsuc  7699  r0weon  7787  infxpenlem  7788  infxpenc2lem2  7794  dfac3  7895  dfac5lem2  7898  dfac5lem3  7899  dfac5lem4  7900  cdafn  7942  unctb  7978  axcc2lem  8209  axdc3lem  8223  axdc4lem  8228  enqex  8693  nqex  8694  enrex  8839  axcnex  8916  zexALT  10193  cnexALT  10501  addex  10503  mulex  10504  ixxex  10820  shftfval  11772  climconst2  12229  xpnnenOLD  12696  cpnnen  12715  ruclem13  12728  cnso  12733  prdsval  13565  prdsplusg  13568  prdsmulr  13569  prdsvsca  13570  prdsle  13571  prdsds  13573  prdshom  13576  prdsco  13577  fnmrc  13719  mrcfval  13720  mreacs  13770  comfffval  13811  oppccofval  13829  sectfval  13864  brssc  13901  sscpwex  13902  isssc  13907  isfunc  13948  isfuncd  13949  idfu2nd  13961  idfu1st  13963  idfucl  13965  wunfunc  13983  fuccofval  14043  homafval  14071  homaf  14072  homaval  14073  coapm  14113  catccofval  14142  catcfuccl  14151  fnxpc  14160  xpcval  14161  xpcbas  14162  xpchom  14164  xpccofval  14166  1stfval  14175  2ndfval  14178  1stfcl  14181  2ndfcl  14182  catcxpccl  14191  evlf2  14202  evlf1  14204  evlfcl  14206  hof1fval  14237  hof2fval  14239  hofcl  14243  ipoval  14467  letsr  14559  plusffval  14589  frmdplusg  14686  eqgfval  14875  efglem  15235  efgval  15236  scaffval  15855  psrplusg  16336  ltbval  16423  opsrle  16427  evlslem2  16459  cnfldds  16603  xrsadd  16608  xrsmul  16609  xrsle  16611  xrsds  16631  znle  16707  ipffval  16769  pjfval  16823  2ndcctbss  17398  txuni2  17477  txbas  17479  eltx  17480  txcnp  17531  txcnmpt  17535  txrest  17542  txlm  17559  tx1stc  17561  tx2ndc  17562  txkgen  17563  txflf  17914  distgp  17995  indistgp  17996  ishtpy  18685  isphtpc  18707  elovolm  19049  elovolmr  19050  ovolmge0  19051  ovolgelb  19054  ovolunlem1a  19070  ovolunlem1  19071  ovoliunlem1  19076  ovoliunlem2  19077  ovolshftlem2  19084  ovolicc2  19096  ioombl1  19134  dyadmbl  19170  vitali  19183  mbfimaopnlem  19225  dvfval  19462  evlssca  19621  mpfind  19643  pf1ind  19653  plyeq0lem  19807  taylfval  19953  ulmval  19974  dmarea  20474  dchrplusg  20709  iseupa  21199  isgrpoi  21297  vcoprne  21569  sspval  21733  0ofval  21799  ajfval  21821  hvmulex  22025  tpr2rico  23786  ustfn  23827  ustn0  23844  ussid  23879  ressuss  23882  faeval  24181  mbfmco2  24199  br2base  24203  sxbrsigalem0  24205  sxbrsigalem3  24206  dya2iocrfn  24213  dya2iocct  24214  dya2iocnrect  24215  dya2iocuni  24217  dya2iocucvr  24218  sxbrsigalem2  24220  sxbrsiga  24224  cvmlift2lem9  24566  brimg  25302  brrestrict  25314  axlowdimlem15  25411  axlowdim  25416  colinearex  25510  heiborlem3  26128  rrnval  26142  ismrer1  26153  mzpincl  26403  pellexlem3  26507  pellexlem4  26508  pellexlem5  26509  aomclem6  26747  lcvfbr  29269  cmtfvalN  29459  cvrfval  29517  dvhvbase  31336  dvhfvadd  31340  dvhfvsca  31349  dibval  31391  dibfna  31403  dicval  31425  hdmap1fval  32046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-rex 2634  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-opab 4180  df-xp 4798
  Copyright terms: Public domain W3C validator