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

Theorem xpex 4800
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 4799 . 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 1685   _Vcvv 2789    X. cxp 4686
This theorem is referenced by:  oprabex  5923  oprabex3  5924  fnpm  6776  mapsnf1o2  6811  ixpsnf1o  6852  xpsnen  6942  endisj  6945  xpcomen  6949  xpassen  6952  xpmapenlem  7024  mapunen  7026  unxpdomlem3  7065  hartogslem1  7253  rankxpl  7543  rankxplim  7545  rankxplim2  7546  rankxplim3  7547  rankxpsuc  7548  r0weon  7636  infxpenlem  7637  infxpenc2lem2  7643  dfac3  7744  dfac5lem2  7747  dfac5lem3  7748  dfac5lem4  7749  cdafn  7791  unctb  7827  axcc2lem  8058  axdc3lem  8072  axdc4lem  8077  enqex  8542  nqex  8543  enrex  8688  axcnex  8765  zexALT  10038  cnexALT  10346  addex  10348  mulex  10349  ixxex  10663  shftfval  11561  climconst2  12018  xpnnenOLD  12484  cpnnen  12503  ruclem13  12516  cnso  12521  prdsval  13351  prdsplusg  13354  prdsmulr  13355  prdsvsca  13356  prdsle  13357  prdsds  13359  prdshom  13362  prdsco  13363  fnmrc  13505  mrcfval  13506  mreacs  13556  comfffval  13597  oppccofval  13615  sectfval  13650  brssc  13687  sscpwex  13688  isssc  13693  isfunc  13734  isfuncd  13735  idfu2nd  13747  idfu1st  13749  idfucl  13751  wunfunc  13769  fuccofval  13829  homafval  13857  homaf  13858  homaval  13859  coapm  13899  catccofval  13928  catcfuccl  13937  fnxpc  13946  xpcval  13947  xpcbas  13948  xpchom  13950  xpccofval  13952  1stfval  13961  2ndfval  13964  1stfcl  13967  2ndfcl  13968  catcxpccl  13977  evlf2  13988  evlf1  13990  evlfcl  13992  hof1fval  14023  hof2fval  14025  hofcl  14029  ipoval  14253  letsr  14345  plusffval  14375  frmdplusg  14472  eqgfval  14661  efglem  15021  efgval  15022  scaffval  15641  psrplusg  16122  ltbval  16209  opsrle  16213  evlslem2  16245  cnfldds  16385  xrsadd  16387  xrsmul  16388  xrsle  16390  xrsds  16410  znle  16486  ipffval  16548  pjfval  16602  2ndcctbss  17177  txuni2  17256  txbas  17258  eltx  17259  txcnp  17310  txcnmpt  17314  txrest  17321  txlm  17338  tx1stc  17340  tx2ndc  17341  txkgen  17342  txflf  17697  distgp  17778  indistgp  17779  ishtpy  18466  isphtpc  18488  elovolm  18830  elovolmr  18831  ovolmge0  18832  ovolgelb  18835  ovolunlem1a  18851  ovolunlem1  18852  ovoliunlem1  18857  ovoliunlem2  18858  ovolshftlem2  18865  ovolicc2  18877  ioombl1  18915  dyadmbl  18951  vitali  18964  mbfimaopnlem  19006  dvfval  19243  evlssca  19402  mpfind  19424  pf1ind  19434  plyeq0lem  19588  taylfval  19734  ulmval  19755  dmarea  20248  dchrplusg  20482  isgrpoi  20859  vcoprne  21129  sspval  21293  0ofval  21359  ajfval  21381  hvmulex  21587  cvmlift2lem9  23249  iseupa  23288  brimg  23886  brrestrict  23897  axlowdimlem15  23994  axlowdim  23999  colinearex  24093  nZdef  24591  issubcat  25256  heiborlem3  25948  rrnval  25962  ismrer1  25973  mzpincl  26223  pellexlem3  26327  pellexlem4  26328  pellexlem5  26329  aomclem6  26567  lcvfbr  28489  cmtfvalN  28679  cvrfval  28737  dvhvbase  30556  dvhfvadd  30560  dvhfvsca  30569  dibval  30611  dibfna  30623  dicval  30645  hdmap1fval  31266
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rex 2550  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-opab 4079  df-xp 4694
  Copyright terms: Public domain W3C validator