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

Theorem xpex 4982
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 4981 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 654 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2948    X. cxp 4868
This theorem is referenced by:  oprabex  6179  oprabex3  6180  fnpm  7018  mapsnf1o2  7053  ixpsnf1o  7094  xpsnen  7184  endisj  7187  xpcomen  7191  xpassen  7194  xpmapenlem  7266  mapunen  7268  unxpdomlem3  7307  hartogslem1  7503  rankxpl  7793  rankxplim  7795  rankxplim2  7796  rankxplim3  7797  rankxpsuc  7798  r0weon  7886  infxpenlem  7887  infxpenc2lem2  7893  dfac3  7994  dfac5lem2  7997  dfac5lem3  7998  dfac5lem4  7999  cdafn  8041  unctb  8077  axcc2lem  8308  axdc3lem  8322  axdc4lem  8327  enqex  8791  nqex  8792  enrex  8937  axcnex  9014  zexALT  10292  cnexALT  10600  addex  10602  mulex  10603  ixxex  10919  shftfval  11877  climconst2  12334  xpnnenOLD  12801  cpnnen  12820  ruclem13  12833  cnso  12838  prdsval  13670  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  prdsle  13676  prdsds  13678  prdshom  13681  prdsco  13682  fnmrc  13824  mrcfval  13825  mreacs  13875  comfffval  13916  oppccofval  13934  sectfval  13969  brssc  14006  sscpwex  14007  isssc  14012  isfunc  14053  isfuncd  14054  idfu2nd  14066  idfu1st  14068  idfucl  14070  wunfunc  14088  fuccofval  14148  homafval  14176  homaf  14177  homaval  14178  coapm  14218  catccofval  14247  catcfuccl  14256  fnxpc  14265  xpcval  14266  xpcbas  14267  xpchom  14269  xpccofval  14271  1stfval  14280  2ndfval  14283  1stfcl  14286  2ndfcl  14287  catcxpccl  14296  evlf2  14307  evlf1  14309  evlfcl  14311  hof1fval  14342  hof2fval  14344  hofcl  14348  ipoval  14572  letsr  14664  plusffval  14694  frmdplusg  14791  eqgfval  14980  efglem  15340  efgval  15341  scaffval  15960  psrplusg  16437  ltbval  16524  opsrle  16528  evlslem2  16560  cnfldds  16705  xrsadd  16710  xrsmul  16711  xrsle  16713  xrsds  16733  znle  16809  ipffval  16871  pjfval  16925  2ndcctbss  17510  txuni2  17589  txbas  17591  eltx  17592  txcnp  17644  txcnmpt  17648  txrest  17655  txlm  17672  tx1stc  17674  tx2ndc  17675  txkgen  17676  txflf  18030  cnextfval  18085  distgp  18121  indistgp  18122  ustfn  18223  ustn0  18242  ussid  18282  ressuss  18285  ishtpy  18989  isphtpc  19011  elovolm  19363  elovolmr  19364  ovolmge0  19365  ovolgelb  19368  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliunlem2  19391  ovolshftlem2  19398  ovolicc2  19410  ioombl1  19448  dyadmbl  19484  vitali  19497  mbfimaopnlem  19539  dvfval  19776  evlssca  19935  mpfind  19957  pf1ind  19967  plyeq0lem  20121  taylfval  20267  ulmval  20288  dmarea  20788  dchrplusg  21023  iseupa  21679  isgrpoi  21778  vcoprne  22050  sspval  22214  0ofval  22280  ajfval  22302  hvmulex  22506  inftmrel  24242  isinftm  24243  tpr2rico  24302  faeval  24589  mbfmco2  24607  br2base  24611  sxbrsigalem0  24613  sxbrsigalem3  24614  dya2iocrfn  24621  dya2iocct  24622  dya2iocnrect  24623  dya2iocuni  24625  dya2iocucvr  24626  sxbrsigalem2  24628  cvmlift2lem9  24990  brimg  25774  brrestrict  25786  axlowdimlem15  25887  axlowdim  25892  colinearex  25986  mblfinlem  26234  heiborlem3  26513  rrnval  26527  ismrer1  26538  mzpincl  26782  pellexlem3  26885  pellexlem4  26886  pellexlem5  26887  aomclem6  27125  lcvfbr  29755  cmtfvalN  29945  cvrfval  30003  dvhvbase  31822  dvhfvadd  31826  dvhfvsca  31835  dibval  31877  dibfna  31889  dicval  31911  hdmap1fval  32532
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-opab 4259  df-xp 4876
  Copyright terms: Public domain W3C validator