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

Theorem xpex 6604
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
xpex.2
Assertion
Ref Expression
xpex

Proof of Theorem xpex
StepHypRef Expression
1 xpex.1 . 2
2 xpex.2 . 2
3 xpexg 6602 . 2
41, 2, 3mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  X.cxp 5002
This theorem is referenced by:  oprabex  6788  oprabex3  6789  fnpm  7447  mapsnf1o2  7486  ixpsnf1o  7529  xpsnen  7621  endisj  7624  xpcomen  7628  xpassen  7631  xpmapenlem  7704  mapunen  7706  unxpdomlem3  7746  hartogslem1  7988  rankxpl  8314  rankfu  8316  rankmapu  8317  rankxplim  8318  rankxplim2  8319  rankxplim3  8320  rankxpsuc  8321  r0weon  8411  infxpenlem  8412  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  dfac3  8523  dfac5lem2  8526  dfac5lem3  8527  dfac5lem4  8528  cdafn  8570  unctb  8606  axcc2lem  8837  axdc3lem  8851  axdc4lem  8856  enqex  9321  nqex  9322  enrex  9465  axcnex  9545  zexALT  10908  cnexALT  11245  addex  11247  mulex  11248  ixxex  11569  shftfval  12903  climconst2  13371  xpnnenOLD  13943  cpnnen  13962  ruclem13  13975  cnso  13980  prdsval  14852  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdsle  14859  prdsds  14861  prdshom  14864  prdsco  14865  fnmrc  15004  mrcfval  15005  mreacs  15055  comfffval  15093  oppccofval  15111  sectfval  15146  brssc  15183  sscpwex  15184  isssc  15189  isfunc  15233  isfuncd  15234  idfu2nd  15246  idfu1st  15248  idfucl  15250  wunfunc  15268  fuccofval  15328  homafval  15356  homaf  15357  homaval  15358  coapm  15398  catccofval  15427  catcfuccl  15436  xpcval  15446  xpcbas  15447  xpchom  15449  xpccofval  15451  1stfval  15460  2ndfval  15463  1stfcl  15466  2ndfcl  15467  catcxpccl  15476  evlf2  15487  evlf1  15489  evlfcl  15491  hof1fval  15522  hof2fval  15524  hofcl  15528  ipoval  15784  letsr  15857  plusffval  15877  frmdplusg  16022  eqgfval  16249  efglem  16734  efgval  16735  scaffval  17530  psrplusg  18034  ltbval  18136  opsrle  18140  evlslem2  18180  evlssca  18191  mpfind  18205  evls1sca  18360  pf1ind  18391  cnfldds  18430  xrsadd  18435  xrsmul  18436  xrsle  18438  xrsds  18461  znle  18573  ipffval  18683  pjfval  18737  mat1dimmul  18978  2ndcctbss  19956  txuni2  20066  txbas  20068  eltx  20069  txcnp  20121  txcnmpt  20125  txrest  20132  txlm  20149  tx1stc  20151  tx2ndc  20152  txkgen  20153  txflf  20507  cnextfval  20562  distgp  20598  indistgp  20599  ustfn  20704  ustn0  20723  ussid  20763  ressuss  20766  ishtpy  21472  isphtpc  21494  elovolm  21886  elovolmr  21887  ovolmge0  21888  ovolgelb  21891  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovolshftlem2  21921  ovolicc2  21933  ioombl1  21972  dyadmbl  22009  vitali  22022  mbfimaopnlem  22062  dvfval  22301  plyeq0lem  22607  taylfval  22754  ulmval  22775  dmarea  23287  dchrplusg  23522  iscgrg  23904  ishlg  23986  ishpg  24128  iscgra  24169  axlowdimlem15  24259  axlowdim  24264  iseupa  24965  numclwwlk1  25098  isgrpoi  25200  vcoprne  25472  sspval  25636  0ofval  25702  ajfval  25724  hvmulex  25928  inftmrel  27724  isinftm  27725  tpr2rico  27894  faeval  28218  mbfmco2  28236  br2base  28240  sxbrsigalem0  28242  sxbrsigalem3  28243  dya2iocrfn  28250  dya2iocct  28251  dya2iocnrect  28252  dya2iocuni  28254  dya2iocucvr  28255  sxbrsigalem2  28257  eulerpartlemgs2  28319  ccatmulgnn0dir  28496  afsval  28551  cvmlift2lem9  28756  mexval  28862  mdvval  28864  mpstval  28895  brimg  29587  brrestrict  29599  colinearex  29710  mblfinlem1  30051  heiborlem3  30309  rrnval  30323  ismrer1  30334  mzpincl  30666  pellexlem3  30767  pellexlem4  30768  pellexlem5  30769  aomclem6  31005  aacllem  33216  lcvfbr  34745  cmtfvalN  34935  cvrfval  34993  dvhvbase  36814  dvhfvadd  36818  dvhfvsca  36827  dibval  36869  dibfna  36881  dicval  36903  hdmap1fval  37524  trclub  37784  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator