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

Theorem xpex 6621
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  |-  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 6620 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 672 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   _Vcvv 3078    X. cxp 4949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2805  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-opab 4462  df-xp 4957
This theorem is referenced by:  oprabex  6678  oprabex3  6679  fnpm  7335  mapsnf1o2  7373  ixpsnf1o  7416  xpsnen  7508  endisj  7511  xpcomen  7515  xpassen  7518  xpmapenlem  7591  mapunen  7593  unxpdomlem3  7633  hartogslem1  7870  rankxpl  8196  rankfu  8198  rankmapu  8199  rankxplim  8200  rankxplim2  8201  rankxplim3  8202  rankxpsuc  8203  r0weon  8293  infxpenlem  8294  infxpenc2lem2  8300  infxpenc2lem2OLD  8304  dfac3  8405  dfac5lem2  8408  dfac5lem3  8409  dfac5lem4  8410  cdafn  8452  unctb  8488  axcc2lem  8719  axdc3lem  8733  axdc4lem  8738  enqex  9205  nqex  9206  enrex  9351  axcnex  9428  zexALT  10779  cnexALT  11101  addex  11103  mulex  11104  ixxex  11425  shftfval  12680  climconst2  13147  xpnnenOLD  13613  cpnnen  13632  ruclem13  13645  cnso  13650  prdsval  14515  prdsplusg  14518  prdsmulr  14519  prdsvsca  14520  prdsle  14522  prdsds  14524  prdshom  14527  prdsco  14528  fnmrc  14667  mrcfval  14668  mreacs  14718  comfffval  14759  oppccofval  14777  sectfval  14812  brssc  14849  sscpwex  14850  isssc  14855  isfunc  14896  isfuncd  14897  idfu2nd  14909  idfu1st  14911  idfucl  14913  wunfunc  14931  fuccofval  14991  homafval  15019  homaf  15020  homaval  15021  coapm  15061  catccofval  15090  catcfuccl  15099  xpcval  15109  xpcbas  15110  xpchom  15112  xpccofval  15114  1stfval  15123  2ndfval  15126  1stfcl  15129  2ndfcl  15130  catcxpccl  15139  evlf2  15150  evlf1  15152  evlfcl  15154  hof1fval  15185  hof2fval  15187  hofcl  15191  ipoval  15446  letsr  15519  plusffval  15549  frmdplusg  15654  eqgfval  15851  efglem  16337  efgval  16338  scaffval  17092  psrplusg  17578  ltbval  17680  opsrle  17684  evlslem2  17724  evlssca  17735  mpfind  17749  evls1sca  17886  pf1ind  17917  cnfldds  17956  xrsadd  17961  xrsmul  17962  xrsle  17964  xrsds  17984  znle  18095  ipffval  18205  pjfval  18259  2ndcctbss  19194  txuni2  19273  txbas  19275  eltx  19276  txcnp  19328  txcnmpt  19332  txrest  19339  txlm  19356  tx1stc  19358  tx2ndc  19359  txkgen  19360  txflf  19714  cnextfval  19769  distgp  19805  indistgp  19806  ustfn  19911  ustn0  19930  ussid  19970  ressuss  19973  ishtpy  20679  isphtpc  20701  elovolm  21093  elovolmr  21094  ovolmge0  21095  ovolgelb  21098  ovolunlem1a  21114  ovolunlem1  21115  ovoliunlem1  21120  ovoliunlem2  21121  ovolshftlem2  21128  ovolicc2  21140  ioombl1  21179  dyadmbl  21216  vitali  21229  mbfimaopnlem  21269  dvfval  21508  plyeq0lem  21814  taylfval  21960  ulmval  21981  dmarea  22487  dchrplusg  22722  iscgrg  23104  axlowdimlem15  23374  axlowdim  23379  iseupa  23758  isgrpoi  23857  vcoprne  24129  sspval  24293  0ofval  24359  ajfval  24381  hvmulex  24585  inftmrel  26362  isinftm  26363  tpr2rico  26507  faeval  26826  mbfmco2  26844  br2base  26848  sxbrsigalem0  26850  sxbrsigalem3  26851  dya2iocrfn  26858  dya2iocct  26859  dya2iocnrect  26860  dya2iocuni  26862  dya2iocucvr  26863  sxbrsigalem2  26865  eulerpartlemgs2  26927  ccatmulgnn0dir  27104  afsval  27159  cvmlift2lem9  27364  brimg  28132  brrestrict  28144  colinearex  28255  mblfinlem1  28596  heiborlem3  28880  rrnval  28894  ismrer1  28905  mzpincl  29238  pellexlem3  29340  pellexlem4  29341  pellexlem5  29342  aomclem6  29580  numclwwlk1  30859  mat1dimmul  31058  lcvfbr  33023  cmtfvalN  33213  cvrfval  33271  dvhvbase  35090  dvhfvadd  35094  dvhfvsca  35103  dibval  35145  dibfna  35157  dicval  35179  hdmap1fval  35800
  Copyright terms: Public domain W3C validator