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

Theorem xpex 6622
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 683 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   _Vcvv 3057    X. cxp 4851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-opab 4476  df-xp 4859  df-rel 4860
This theorem is referenced by:  oprabex  6808  oprabex3  6809  fnpm  7506  mapsnf1o2  7545  ixpsnf1o  7588  xpsnen  7682  endisj  7685  xpcomen  7689  xpassen  7692  xpmapenlem  7765  mapunen  7767  unxpdomlem3  7804  hartogslem1  8083  rankxpl  8372  rankfu  8374  rankmapu  8375  rankxplim  8376  rankxplim2  8377  rankxplim3  8378  rankxpsuc  8379  r0weon  8469  infxpenlem  8470  infxpenc2lem2  8477  dfac3  8578  dfac5lem2  8581  dfac5lem3  8582  dfac5lem4  8583  cdafn  8625  unctb  8661  axcc2lem  8892  axdc3lem  8906  axdc4lem  8911  enqex  9373  nqex  9374  enrex  9517  axcnex  9597  zexALT  10985  cnexALT  11327  addex  11329  mulex  11330  ixxex  11675  shftfval  13182  climconst2  13661  cpnnen  14330  ruclem13  14343  cnso  14348  prdsval  15402  prdsplusg  15405  prdsmulr  15406  prdsvsca  15407  prdsle  15409  prdsds  15411  prdshom  15414  prdsco  15415  fnmrc  15562  mrcfval  15563  mreacs  15613  comfffval  15652  oppccofval  15670  sectfval  15705  brssc  15768  sscpwex  15769  isssc  15774  isfunc  15818  isfuncd  15819  idfu2nd  15831  idfu1st  15833  idfucl  15835  wunfunc  15853  fuccofval  15913  homafval  15973  homaf  15974  homaval  15975  coapm  16015  catccofval  16044  catcfuccl  16053  xpcval  16111  xpcbas  16112  xpchom  16114  xpccofval  16116  1stfval  16125  2ndfval  16128  1stfcl  16131  2ndfcl  16132  catcxpccl  16141  evlf2  16152  evlf1  16154  evlfcl  16156  hof1fval  16187  hof2fval  16189  hofcl  16193  ipoval  16449  letsr  16522  plusffval  16542  frmdplusg  16687  eqgfval  16914  efglem  17415  efgval  17416  scaffval  18158  psrplusg  18654  ltbval  18744  opsrle  18748  evlslem2  18784  evlssca  18794  mpfind  18808  evls1sca  18961  pf1ind  18992  cnfldds  19029  xrsadd  19034  xrsmul  19035  xrsle  19037  xrsds  19060  znle  19156  ipffval  19264  pjfval  19318  mat1dimmul  19550  2ndcctbss  20519  txuni2  20629  txbas  20631  eltx  20632  txcnp  20684  txcnmpt  20688  txrest  20695  txlm  20712  tx1stc  20714  tx2ndc  20715  txkgen  20716  txflf  21070  cnextfval  21126  distgp  21163  indistgp  21164  ustfn  21265  ustn0  21284  ussid  21324  ressuss  21327  ishtpy  22052  isphtpc  22074  elovolm  22477  elovolmr  22478  ovolmge0  22479  ovolgelb  22482  ovolunlem1a  22498  ovolunlem1  22499  ovoliunlem1  22504  ovoliunlem2  22505  ovolshftlem2  22512  ovolicc2  22525  ioombl1  22564  dyadmbl  22607  vitali  22620  mbfimaopnlem  22660  dvfval  22901  plyeq0lem  23213  taylfval  23363  ulmval  23384  dmarea  23932  dchrplusg  24224  iscgrg  24606  ishlg  24696  ishpg  24850  iscgra  24900  isinag  24928  axlowdimlem15  25035  axlowdim  25040  iseupa  25742  numclwwlk1  25875  isgrpoi  25975  vcoprne  26247  sspval  26411  0ofval  26477  ajfval  26499  hvmulex  26713  inftmrel  28546  isinftm  28547  smatrcl  28671  tpr2rico  28767  faeval  29118  mbfmco2  29136  br2base  29140  sxbrsigalem0  29142  sxbrsigalem3  29143  dya2iocrfn  29150  dya2iocct  29151  dya2iocnrect  29152  dya2iocuni  29154  dya2iocucvr  29155  sxbrsigalem2  29157  eulerpartlemgs2  29262  ccatmulgnn0dir  29477  afsval  29537  cvmlift2lem9  30083  mexval  30189  mdvval  30191  mpstval  30222  brimg  30753  brrestrict  30765  colinearex  30876  poimirlem4  31989  poimirlem28  32013  mblfinlem1  32022  heiborlem3  32190  rrnval  32204  ismrer1  32215  lcvfbr  32631  cmtfvalN  32821  cvrfval  32879  dvhvbase  34700  dvhfvadd  34704  dvhfvsca  34713  dibval  34755  dibfna  34767  dicval  34789  hdmap1fval  35410  mzpincl  35621  pellexlem3  35720  pellexlem4  35721  pellexlem5  35722  aomclem6  35962  trclexi  36272  rtrclexi  36273  brtrclfv2  36364  hoiprodcl2  38415  hoicvrrex  38416  ovn0lem  38425  ovnhoilem1  38461  ovnlecvr2  38470  opnvonmbllem1  38492  opnvonmbllem2  38493  aacllem  40813
  Copyright terms: Public domain W3C validator