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

Theorem xpex 4803
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 4802 . 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 1686   _Vcvv 2790    X. cxp 4689
This theorem is referenced by:  oprabex  5963  oprabex3  5964  fnpm  6782  mapsnf1o2  6817  ixpsnf1o  6858  xpsnen  6948  endisj  6951  xpcomen  6955  xpassen  6958  xpmapenlem  7030  mapunen  7032  unxpdomlem3  7071  hartogslem1  7259  rankxpl  7549  rankxplim  7551  rankxplim2  7552  rankxplim3  7553  rankxpsuc  7554  r0weon  7642  infxpenlem  7643  infxpenc2lem2  7649  dfac3  7750  dfac5lem2  7753  dfac5lem3  7754  dfac5lem4  7755  cdafn  7797  unctb  7833  axcc2lem  8064  axdc3lem  8078  axdc4lem  8083  enqex  8548  nqex  8549  enrex  8694  axcnex  8771  zexALT  10044  cnexALT  10352  addex  10354  mulex  10355  ixxex  10669  shftfval  11567  climconst2  12024  xpnnenOLD  12490  cpnnen  12509  ruclem13  12522  cnso  12527  prdsval  13357  prdsplusg  13360  prdsmulr  13361  prdsvsca  13362  prdsle  13363  prdsds  13365  prdshom  13368  prdsco  13369  fnmrc  13511  mrcfval  13512  mreacs  13562  comfffval  13603  oppccofval  13621  sectfval  13656  brssc  13693  sscpwex  13694  isssc  13699  isfunc  13740  isfuncd  13741  idfu2nd  13753  idfu1st  13755  idfucl  13757  wunfunc  13775  fuccofval  13835  homafval  13863  homaf  13864  homaval  13865  coapm  13905  catccofval  13934  catcfuccl  13943  fnxpc  13952  xpcval  13953  xpcbas  13954  xpchom  13956  xpccofval  13958  1stfval  13967  2ndfval  13970  1stfcl  13973  2ndfcl  13974  catcxpccl  13983  evlf2  13994  evlf1  13996  evlfcl  13998  hof1fval  14029  hof2fval  14031  hofcl  14035  ipoval  14259  letsr  14351  plusffval  14381  frmdplusg  14478  eqgfval  14667  efglem  15027  efgval  15028  scaffval  15647  psrplusg  16128  ltbval  16215  opsrle  16219  evlslem2  16251  cnfldds  16391  xrsadd  16393  xrsmul  16394  xrsle  16396  xrsds  16416  znle  16492  ipffval  16554  pjfval  16608  2ndcctbss  17183  txuni2  17262  txbas  17264  eltx  17265  txcnp  17316  txcnmpt  17320  txrest  17327  txlm  17344  tx1stc  17346  tx2ndc  17347  txkgen  17348  txflf  17703  distgp  17784  indistgp  17785  ishtpy  18472  isphtpc  18494  elovolm  18836  elovolmr  18837  ovolmge0  18838  ovolgelb  18841  ovolunlem1a  18857  ovolunlem1  18858  ovoliunlem1  18863  ovoliunlem2  18864  ovolshftlem2  18871  ovolicc2  18883  ioombl1  18921  dyadmbl  18957  vitali  18970  mbfimaopnlem  19012  dvfval  19249  evlssca  19408  mpfind  19430  pf1ind  19440  plyeq0lem  19594  taylfval  19740  ulmval  19761  dmarea  20254  dchrplusg  20488  isgrpoi  20867  vcoprne  21137  sspval  21301  0ofval  21367  ajfval  21389  hvmulex  21593  tpr2rico  23298  mbfmco2  23572  br2base  23576  dya2iocct  23583  dya2iocrrnval  23584  cvmlift2lem9  23844  iseupa  23883  brimg  24478  brrestrict  24489  axlowdimlem15  24586  axlowdim  24591  colinearex  24685  nZdef  25191  issubcat  25856  heiborlem3  26548  rrnval  26562  ismrer1  26573  mzpincl  26823  pellexlem3  26927  pellexlem4  26928  pellexlem5  26929  aomclem6  27167  lcvfbr  29283  cmtfvalN  29473  cvrfval  29531  dvhvbase  31350  dvhfvadd  31354  dvhfvsca  31363  dibval  31405  dibfna  31417  dicval  31439  hdmap1fval  32060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rex 2551  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-opab 4080  df-xp 4697
  Copyright terms: Public domain W3C validator