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

Theorem xpex 7464
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 𝐴 ∈ V
xpex.2 𝐵 ∈ V
Assertion
Ref Expression
xpex (𝐴 × 𝐵) ∈ V

Proof of Theorem xpex
StepHypRef Expression
1 xpex.1 . 2 𝐴 ∈ V
2 xpex.2 . 2 𝐵 ∈ V
3 xpexg 7461 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
41, 2, 3mp2an 688 1 (𝐴 × 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495   × cxp 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-opab 5121  df-xp 5555  df-rel 5556
This theorem is referenced by:  oprabex  7668  oprabex3  7669  mpoexw  7767  fnpm  8404  mapsnf1o2  8447  ixpsnf1o  8491  xpsnen  8590  endisj  8593  xpcomen  8597  xpassen  8600  xpmapenlem  8673  mapunen  8675  unxpdomlem3  8713  hartogslem1  8995  rankxpl  9293  rankfu  9295  rankmapu  9296  rankxplim  9297  rankxplim2  9298  rankxplim3  9299  rankxpsuc  9300  r0weon  9427  infxpenlem  9428  infxpenc2lem2  9435  dfac3  9536  dfac5lem2  9539  dfac5lem3  9540  dfac5lem4  9541  unctb  9616  axcc2lem  9847  axdc3lem  9861  axdc4lem  9866  enqex  10333  nqex  10334  nrex1  10475  enrex  10478  axcnex  10558  zexALT  11990  cnexALT  12375  addex  12377  mulex  12378  ixxex  12739  shftfval  14419  climconst2  14895  cpnnen  15572  ruclem13  15585  cnso  15590  prdsval  16718  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  prdsle  16725  prdsds  16727  prdshom  16730  prdsco  16731  fnmrc  16868  mrcfval  16869  mreacs  16919  comfffval  16958  oppccofval  16976  sectfval  17011  brssc  17074  sscpwex  17075  isssc  17080  isfunc  17124  isfuncd  17125  idfu2nd  17137  idfu1st  17139  idfucl  17141  wunfunc  17159  fuccofval  17219  homafval  17279  homaf  17280  homaval  17281  coapm  17321  catccofval  17350  catcfuccl  17359  xpcval  17417  xpcbas  17418  xpchom  17420  xpccofval  17422  1stfval  17431  2ndfval  17434  1stfcl  17437  2ndfcl  17438  catcxpccl  17447  evlf2  17458  evlf1  17460  evlfcl  17462  hof1fval  17493  hof2fval  17495  hofcl  17499  ipoval  17754  letsr  17827  frmdplusg  18009  eqgfval  18268  efglem  18773  efgval  18774  psrplusg  20091  ltbval  20182  opsrle  20186  evlslem2  20222  evlssca  20232  mpfind  20250  evls1sca  20416  pf1ind  20448  cnfldds  20485  cnfldfun  20487  cnfldfunALT  20488  xrsadd  20492  xrsmul  20493  xrsle  20495  xrsds  20518  znle  20613  pjfval  20780  mat1dimmul  21015  2ndcctbss  21993  txuni2  22103  txbas  22105  eltx  22106  txcnp  22158  txcnmpt  22162  txrest  22169  txlm  22186  tx1stc  22188  tx2ndc  22189  txkgen  22190  txflf  22544  cnextfval  22600  distgp  22637  indistgp  22638  ustfn  22739  ustn0  22758  ussid  22798  ressuss  22801  ishtpy  23505  isphtpc  23527  elovolmlem  24004  dyadmbl  24130  vitali  24143  mbfimaopnlem  24185  dvfval  24424  plyeq0lem  24729  taylfval  24876  ulmval  24897  dmarea  25463  dchrplusg  25751  tgjustc1  26189  tgjustc2  26190  iscgrg  26226  ishlg  26316  ishpg  26473  iscgra  26523  isinag  26552  isleag  26561  axlowdimlem15  26670  axlowdim  26675  isgrpoi  28203  sspval  28428  0ofval  28492  ajfval  28514  hvmulex  28716  inftmrel  30737  isinftm  30738  smatrcl  30961  tpr2rico  31055  faeval  31405  mbfmco2  31423  br2base  31427  sxbrsigalem0  31429  sxbrsigalem3  31430  dya2iocrfn  31437  dya2iocct  31438  dya2iocnrect  31439  dya2iocuni  31441  dya2iocucvr  31442  sxbrsigalem2  31444  eulerpartlemgs2  31538  ccatmulgnn0dir  31712  afsval  31842  cvmlift2lem9  32456  satfv0  32503  satf00  32519  prv1n  32576  mexval  32647  mdvval  32649  mpstval  32680  brimg  33296  brrestrict  33308  colinearex  33419  poimirlem4  34778  poimirlem28  34802  mblfinlem1  34811  heiborlem3  34974  rrnval  34988  ismrer1  34999  dfcnvrefrels2  35648  dfcnvrefrels3  35649  lcvfbr  36038  cmtfvalN  36228  cvrfval  36286  dvhvbase  38105  dvhfvadd  38109  dvhfvsca  38118  dibval  38160  dibfna  38172  dicval  38194  hdmap1fval  38814  mzpincl  39211  pellexlem3  39308  pellexlem4  39309  pellexlem5  39310  aomclem6  39539  trclexi  39860  rtrclexi  39861  brtrclfv2  39952  hoiprodcl2  42718  hoicvrrex  42719  ovn0lem  42728  ovnhoilem1  42764  ovnlecvr2  42773  opnvonmbllem1  42795  opnvonmbllem2  42796  ovolval2lem  42806  ovolval2  42807  ovolval3  42810  ovolval4lem2  42813  ovolval5lem2  42816  ovnovollem1  42819  ovnovollem2  42820  smflimlem6  42933  elpglem3  44713  aacllem  44800
  Copyright terms: Public domain W3C validator