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

Theorem xpex 6497
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 6496 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 665 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   _Vcvv 2962    X. cxp 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-rex 2711  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-opab 4339  df-xp 4833
This theorem is referenced by:  oprabex  6554  oprabex3  6555  fnpm  7210  mapsnf1o2  7248  ixpsnf1o  7291  xpsnen  7383  endisj  7386  xpcomen  7390  xpassen  7393  xpmapenlem  7466  mapunen  7468  unxpdomlem3  7507  hartogslem1  7744  rankxpl  8070  rankfu  8072  rankmapu  8073  rankxplim  8074  rankxplim2  8075  rankxplim3  8076  rankxpsuc  8077  r0weon  8167  infxpenlem  8168  infxpenc2lem2  8174  infxpenc2lem2OLD  8178  dfac3  8279  dfac5lem2  8282  dfac5lem3  8283  dfac5lem4  8284  cdafn  8326  unctb  8362  axcc2lem  8593  axdc3lem  8607  axdc4lem  8612  enqex  9078  nqex  9079  enrex  9224  axcnex  9301  zexALT  10652  cnexALT  10974  addex  10976  mulex  10977  ixxex  11298  shftfval  12542  climconst2  13009  xpnnenOLD  13474  cpnnen  13493  ruclem13  13506  cnso  13511  prdsval  14375  prdsplusg  14378  prdsmulr  14379  prdsvsca  14380  prdsle  14382  prdsds  14384  prdshom  14387  prdsco  14388  fnmrc  14527  mrcfval  14528  mreacs  14578  comfffval  14619  oppccofval  14637  sectfval  14672  brssc  14709  sscpwex  14710  isssc  14715  isfunc  14756  isfuncd  14757  idfu2nd  14769  idfu1st  14771  idfucl  14773  wunfunc  14791  fuccofval  14851  homafval  14879  homaf  14880  homaval  14881  coapm  14921  catccofval  14950  catcfuccl  14959  xpcval  14969  xpcbas  14970  xpchom  14972  xpccofval  14974  1stfval  14983  2ndfval  14986  1stfcl  14989  2ndfcl  14990  catcxpccl  14999  evlf2  15010  evlf1  15012  evlfcl  15014  hof1fval  15045  hof2fval  15047  hofcl  15051  ipoval  15306  letsr  15379  plusffval  15409  frmdplusg  15511  eqgfval  15708  efglem  16192  efgval  16193  scaffval  16889  psrplusg  17385  ltbval  17484  opsrle  17488  evlslem2  17524  cnfldds  17671  xrsadd  17676  xrsmul  17677  xrsle  17679  xrsds  17699  znle  17808  ipffval  17918  pjfval  17972  2ndcctbss  18900  txuni2  18979  txbas  18981  eltx  18982  txcnp  19034  txcnmpt  19038  txrest  19045  txlm  19062  tx1stc  19064  tx2ndc  19065  txkgen  19066  txflf  19420  cnextfval  19475  distgp  19511  indistgp  19512  ustfn  19617  ustn0  19636  ussid  19676  ressuss  19679  ishtpy  20385  isphtpc  20407  elovolm  20799  elovolmr  20800  ovolmge0  20801  ovolgelb  20804  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliunlem2  20827  ovolshftlem2  20834  ovolicc2  20846  ioombl1  20884  dyadmbl  20921  vitali  20934  mbfimaopnlem  20974  dvfval  21213  evlssca  21373  mpfind  21395  pf1ind  21405  plyeq0lem  21562  taylfval  21708  ulmval  21729  dmarea  22235  dchrplusg  22470  iscgrg  22845  axlowdimlem15  23024  axlowdim  23029  iseupa  23408  isgrpoi  23507  vcoprne  23779  sspval  23943  0ofval  24009  ajfval  24031  hvmulex  24235  inftmrel  26020  isinftm  26021  tpr2rico  26195  faeval  26515  mbfmco2  26533  br2base  26537  sxbrsigalem0  26539  sxbrsigalem3  26540  dya2iocrfn  26547  dya2iocct  26548  dya2iocnrect  26549  dya2iocuni  26551  dya2iocucvr  26552  sxbrsigalem2  26554  eulerpartlemgs2  26610  ccatmulgnn0dir  26787  afsval  26842  cvmlift2lem9  27047  brimg  27814  brrestrict  27826  colinearex  27937  mblfinlem1  28269  heiborlem3  28553  rrnval  28567  ismrer1  28578  mzpincl  28912  pellexlem3  29014  pellexlem4  29015  pellexlem5  29016  aomclem6  29254  numclwwlk1  30534  lcvfbr  32235  cmtfvalN  32425  cvrfval  32483  dvhvbase  34302  dvhfvadd  34306  dvhfvsca  34315  dibval  34357  dibfna  34369  dicval  34391  hdmap1fval  35012
  Copyright terms: Public domain W3C validator