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

Theorem xpex 6585
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 6583 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 670 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842   _Vcvv 3058    X. cxp 4820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-opab 4453  df-xp 4828  df-rel 4829
This theorem is referenced by:  oprabex  6771  oprabex3  6772  fnpm  7464  mapsnf1o2  7503  ixpsnf1o  7546  xpsnen  7638  endisj  7641  xpcomen  7645  xpassen  7648  xpmapenlem  7721  mapunen  7723  unxpdomlem3  7760  hartogslem1  8000  rankxpl  8324  rankfu  8326  rankmapu  8327  rankxplim  8328  rankxplim2  8329  rankxplim3  8330  rankxpsuc  8331  r0weon  8421  infxpenlem  8422  infxpenc2lem2  8428  infxpenc2lem2OLD  8432  dfac3  8533  dfac5lem2  8536  dfac5lem3  8537  dfac5lem4  8538  cdafn  8580  unctb  8616  axcc2lem  8847  axdc3lem  8861  axdc4lem  8866  enqex  9329  nqex  9330  enrex  9473  axcnex  9553  zexALT  10923  cnexALT  11260  addex  11262  mulex  11263  ixxex  11592  shftfval  13050  climconst2  13518  cpnnen  14169  ruclem13  14182  cnso  14187  prdsval  15067  prdsplusg  15070  prdsmulr  15071  prdsvsca  15072  prdsle  15074  prdsds  15076  prdshom  15079  prdsco  15080  fnmrc  15219  mrcfval  15220  mreacs  15270  comfffval  15309  oppccofval  15327  sectfval  15362  brssc  15425  sscpwex  15426  isssc  15431  isfunc  15475  isfuncd  15476  idfu2nd  15488  idfu1st  15490  idfucl  15492  wunfunc  15510  fuccofval  15570  homafval  15630  homaf  15631  homaval  15632  coapm  15672  catccofval  15701  catcfuccl  15710  xpcval  15768  xpcbas  15769  xpchom  15771  xpccofval  15773  1stfval  15782  2ndfval  15785  1stfcl  15788  2ndfcl  15789  catcxpccl  15798  evlf2  15809  evlf1  15811  evlfcl  15813  hof1fval  15844  hof2fval  15846  hofcl  15850  ipoval  16106  letsr  16179  plusffval  16199  frmdplusg  16344  eqgfval  16571  efglem  17056  efgval  17057  scaffval  17848  psrplusg  18352  ltbval  18454  opsrle  18458  evlslem2  18498  evlssca  18509  mpfind  18523  evls1sca  18678  pf1ind  18709  cnfldds  18748  xrsadd  18753  xrsmul  18754  xrsle  18756  xrsds  18779  znle  18871  ipffval  18979  pjfval  19033  mat1dimmul  19268  2ndcctbss  20246  txuni2  20356  txbas  20358  eltx  20359  txcnp  20411  txcnmpt  20415  txrest  20422  txlm  20439  tx1stc  20441  tx2ndc  20442  txkgen  20443  txflf  20797  cnextfval  20852  distgp  20888  indistgp  20889  ustfn  20994  ustn0  21013  ussid  21053  ressuss  21056  ishtpy  21762  isphtpc  21784  elovolm  22176  elovolmr  22177  ovolmge0  22178  ovolgelb  22181  ovolunlem1a  22197  ovolunlem1  22198  ovoliunlem1  22203  ovoliunlem2  22204  ovolshftlem2  22211  ovolicc2  22223  ioombl1  22262  dyadmbl  22299  vitali  22312  mbfimaopnlem  22352  dvfval  22591  plyeq0lem  22897  taylfval  23044  ulmval  23065  dmarea  23611  dchrplusg  23901  iscgrg  24283  ishlg  24368  ishpg  24511  iscgra  24552  axlowdimlem15  24663  axlowdim  24668  iseupa  25369  numclwwlk1  25502  isgrpoi  25600  vcoprne  25872  sspval  26036  0ofval  26102  ajfval  26124  hvmulex  26328  inftmrel  28162  isinftm  28163  tpr2rico  28333  faeval  28681  mbfmco2  28699  br2base  28703  sxbrsigalem0  28705  sxbrsigalem3  28706  dya2iocrfn  28713  dya2iocct  28714  dya2iocnrect  28715  dya2iocuni  28717  dya2iocucvr  28718  sxbrsigalem2  28720  eulerpartlemgs2  28811  ccatmulgnn0dir  28988  afsval  29048  cvmlift2lem9  29595  mexval  29701  mdvval  29703  mpstval  29734  brimg  30262  brrestrict  30274  colinearex  30385  mblfinlem1  31403  heiborlem3  31571  rrnval  31585  ismrer1  31596  lcvfbr  32018  cmtfvalN  32208  cvrfval  32266  dvhvbase  34087  dvhfvadd  34091  dvhfvsca  34100  dibval  34142  dibfna  34154  dicval  34176  hdmap1fval  34797  mzpincl  35008  pellexlem3  35108  pellexlem4  35109  pellexlem5  35110  aomclem6  35347  brtrclfv2  35686  aacllem  38841
  Copyright terms: Public domain W3C validator