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

Theorem xpex 6606
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 6604 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 676 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   _Vcvv 3081    X. cxp 4848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-opab 4480  df-xp 4856  df-rel 4857
This theorem is referenced by:  oprabex  6792  oprabex3  6793  fnpm  7485  mapsnf1o2  7524  ixpsnf1o  7567  xpsnen  7659  endisj  7662  xpcomen  7666  xpassen  7669  xpmapenlem  7742  mapunen  7744  unxpdomlem3  7781  hartogslem1  8060  rankxpl  8348  rankfu  8350  rankmapu  8351  rankxplim  8352  rankxplim2  8353  rankxplim3  8354  rankxpsuc  8355  r0weon  8445  infxpenlem  8446  infxpenc2lem2  8452  dfac3  8553  dfac5lem2  8556  dfac5lem3  8557  dfac5lem4  8558  cdafn  8600  unctb  8636  axcc2lem  8867  axdc3lem  8881  axdc4lem  8886  enqex  9348  nqex  9349  enrex  9492  axcnex  9572  zexALT  10957  cnexALT  11299  addex  11301  mulex  11302  ixxex  11647  shftfval  13122  climconst2  13600  cpnnen  14269  ruclem13  14282  cnso  14287  prdsval  15341  prdsplusg  15344  prdsmulr  15345  prdsvsca  15346  prdsle  15348  prdsds  15350  prdshom  15353  prdsco  15354  fnmrc  15501  mrcfval  15502  mreacs  15552  comfffval  15591  oppccofval  15609  sectfval  15644  brssc  15707  sscpwex  15708  isssc  15713  isfunc  15757  isfuncd  15758  idfu2nd  15770  idfu1st  15772  idfucl  15774  wunfunc  15792  fuccofval  15852  homafval  15912  homaf  15913  homaval  15914  coapm  15954  catccofval  15983  catcfuccl  15992  xpcval  16050  xpcbas  16051  xpchom  16053  xpccofval  16055  1stfval  16064  2ndfval  16067  1stfcl  16070  2ndfcl  16071  catcxpccl  16080  evlf2  16091  evlf1  16093  evlfcl  16095  hof1fval  16126  hof2fval  16128  hofcl  16132  ipoval  16388  letsr  16461  plusffval  16481  frmdplusg  16626  eqgfval  16853  efglem  17354  efgval  17355  scaffval  18097  psrplusg  18593  ltbval  18683  opsrle  18687  evlslem2  18723  evlssca  18733  mpfind  18747  evls1sca  18900  pf1ind  18931  cnfldds  18968  xrsadd  18973  xrsmul  18974  xrsle  18976  xrsds  18999  znle  19094  ipffval  19202  pjfval  19256  mat1dimmul  19488  2ndcctbss  20457  txuni2  20567  txbas  20569  eltx  20570  txcnp  20622  txcnmpt  20626  txrest  20633  txlm  20650  tx1stc  20652  tx2ndc  20653  txkgen  20654  txflf  21008  cnextfval  21064  distgp  21101  indistgp  21102  ustfn  21203  ustn0  21222  ussid  21262  ressuss  21265  ishtpy  21990  isphtpc  22012  elovolm  22415  elovolmr  22416  ovolmge0  22417  ovolgelb  22420  ovolunlem1a  22436  ovolunlem1  22437  ovoliunlem1  22442  ovoliunlem2  22443  ovolshftlem2  22450  ovolicc2  22463  ioombl1  22502  dyadmbl  22545  vitali  22558  mbfimaopnlem  22598  dvfval  22839  plyeq0lem  23151  taylfval  23301  ulmval  23322  dmarea  23870  dchrplusg  24162  iscgrg  24544  ishlg  24634  ishpg  24788  iscgra  24838  isinag  24866  axlowdimlem15  24973  axlowdim  24978  iseupa  25679  numclwwlk1  25812  isgrpoi  25912  vcoprne  26184  sspval  26348  0ofval  26414  ajfval  26436  hvmulex  26650  inftmrel  28492  isinftm  28493  smatrcl  28618  tpr2rico  28714  faeval  29065  mbfmco2  29083  br2base  29087  sxbrsigalem0  29089  sxbrsigalem3  29090  dya2iocrfn  29097  dya2iocct  29098  dya2iocnrect  29099  dya2iocuni  29101  dya2iocucvr  29102  sxbrsigalem2  29104  eulerpartlemgs2  29209  ccatmulgnn0dir  29424  afsval  29484  cvmlift2lem9  30030  mexval  30136  mdvval  30138  mpstval  30169  brimg  30697  brrestrict  30709  colinearex  30820  poimirlem4  31858  poimirlem28  31882  mblfinlem1  31891  heiborlem3  32059  rrnval  32073  ismrer1  32084  lcvfbr  32505  cmtfvalN  32695  cvrfval  32753  dvhvbase  34574  dvhfvadd  34578  dvhfvsca  34587  dibval  34629  dibfna  34641  dicval  34663  hdmap1fval  35284  mzpincl  35495  pellexlem3  35595  pellexlem4  35596  pellexlem5  35597  aomclem6  35837  brtrclfv2  36179  hoiprodcl2  38152  hoicvrrex  38153  ovn0lem  38162  aacllem  39814
  Copyright terms: Public domain W3C validator