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

Theorem xpex 6589
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 6587 . 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 1804   _Vcvv 3095    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rex 2799  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-opab 4496  df-xp 4995
This theorem is referenced by:  oprabex  6773  oprabex3  6774  fnpm  7430  mapsnf1o2  7468  ixpsnf1o  7511  xpsnen  7603  endisj  7606  xpcomen  7610  xpassen  7613  xpmapenlem  7686  mapunen  7688  unxpdomlem3  7728  hartogslem1  7970  rankxpl  8296  rankfu  8298  rankmapu  8299  rankxplim  8300  rankxplim2  8301  rankxplim3  8302  rankxpsuc  8303  r0weon  8393  infxpenlem  8394  infxpenc2lem2  8400  infxpenc2lem2OLD  8404  dfac3  8505  dfac5lem2  8508  dfac5lem3  8509  dfac5lem4  8510  cdafn  8552  unctb  8588  axcc2lem  8819  axdc3lem  8833  axdc4lem  8838  enqex  9303  nqex  9304  enrex  9447  axcnex  9527  zexALT  10890  cnexALT  11227  addex  11229  mulex  11230  ixxex  11551  shftfval  12885  climconst2  13353  xpnnenOLD  13925  cpnnen  13944  ruclem13  13957  cnso  13962  prdsval  14834  prdsplusg  14837  prdsmulr  14838  prdsvsca  14839  prdsle  14841  prdsds  14843  prdshom  14846  prdsco  14847  fnmrc  14986  mrcfval  14987  mreacs  15037  comfffval  15075  oppccofval  15093  sectfval  15128  brssc  15165  sscpwex  15166  isssc  15171  isfunc  15212  isfuncd  15213  idfu2nd  15225  idfu1st  15227  idfucl  15229  wunfunc  15247  fuccofval  15307  homafval  15335  homaf  15336  homaval  15337  coapm  15377  catccofval  15406  catcfuccl  15415  xpcval  15425  xpcbas  15426  xpchom  15428  xpccofval  15430  1stfval  15439  2ndfval  15442  1stfcl  15445  2ndfcl  15446  catcxpccl  15455  evlf2  15466  evlf1  15468  evlfcl  15470  hof1fval  15501  hof2fval  15503  hofcl  15507  ipoval  15763  letsr  15836  plusffval  15856  frmdplusg  16001  eqgfval  16228  efglem  16713  efgval  16714  scaffval  17509  psrplusg  18013  ltbval  18115  opsrle  18119  evlslem2  18159  evlssca  18170  mpfind  18184  evls1sca  18339  pf1ind  18370  cnfldds  18409  xrsadd  18414  xrsmul  18415  xrsle  18417  xrsds  18440  znle  18551  ipffval  18661  pjfval  18715  mat1dimmul  18956  2ndcctbss  19934  txuni2  20044  txbas  20046  eltx  20047  txcnp  20099  txcnmpt  20103  txrest  20110  txlm  20127  tx1stc  20129  tx2ndc  20130  txkgen  20131  txflf  20485  cnextfval  20540  distgp  20576  indistgp  20577  ustfn  20682  ustn0  20701  ussid  20741  ressuss  20744  ishtpy  21450  isphtpc  21472  elovolm  21864  elovolmr  21865  ovolmge0  21866  ovolgelb  21869  ovolunlem1a  21885  ovolunlem1  21886  ovoliunlem1  21891  ovoliunlem2  21892  ovolshftlem2  21899  ovolicc2  21911  ioombl1  21950  dyadmbl  21987  vitali  22000  mbfimaopnlem  22040  dvfval  22279  plyeq0lem  22585  taylfval  22732  ulmval  22753  dmarea  23265  dchrplusg  23500  iscgrg  23882  ishlg  23964  ishpg  24106  iscgra  24147  axlowdimlem15  24237  axlowdim  24242  iseupa  24943  numclwwlk1  25076  isgrpoi  25178  vcoprne  25450  sspval  25614  0ofval  25680  ajfval  25702  hvmulex  25906  inftmrel  27702  isinftm  27703  tpr2rico  27872  faeval  28196  mbfmco2  28214  br2base  28218  sxbrsigalem0  28220  sxbrsigalem3  28221  dya2iocrfn  28228  dya2iocct  28229  dya2iocnrect  28230  dya2iocuni  28232  dya2iocucvr  28233  sxbrsigalem2  28235  eulerpartlemgs2  28297  ccatmulgnn0dir  28474  afsval  28529  cvmlift2lem9  28734  mexval  28840  mdvval  28842  mpstval  28873  brimg  29563  brrestrict  29575  colinearex  29686  mblfinlem1  30027  heiborlem3  30285  rrnval  30299  ismrer1  30310  mzpincl  30642  pellexlem3  30743  pellexlem4  30744  pellexlem5  30745  aomclem6  30981  lcvfbr  34620  cmtfvalN  34810  cvrfval  34868  dvhvbase  36689  dvhfvadd  36693  dvhfvsca  36702  dibval  36744  dibfna  36756  dicval  36778  hdmap1fval  37399  trclub  37612  trclubg  37613
  Copyright terms: Public domain W3C validator