Theorem xpexd 7691

Description: The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
xpexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
xpexd.2	⊢ (𝜑 → 𝐵 ∈ 𝑊)

Assertion

Ref	Expression
xpexd	⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)

Proof of Theorem xpexd

Step	Hyp	Ref	Expression
1		xpexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		xpexd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		xpexg 7690	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3438   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-opab 5158  df-xp 5629  df-rel 5630

This theorem is referenced by:  cnvexg  7864  fabexd  7877  cofunexg  7891  oprabexd  7917  ofmresex  7927  opabex2  7999  offval22  8028  sexp2  8086  sexp3  8093  tposexg  8180  mapunen  9070  marypha1  9343  wdom2d  9491  ixpiunwdom  9501  ttrclexg  9638  fnct  10450  fpwwe2lem2  10545  fpwwe2lem4  10547  fpwwe2lem11  10554  fpwwelem  10558  canthwe  10564  pwxpndom  10579  gchhar  10592  trclexlem  14919  isacs1i  17581  brcic  17723  rescval2  17753  reschom  17755  rescabs  17758  setccofval  18007  estrccofval  18053  sylow2a  19516  gsumxp  19873  gsumxp2  19877  opsrval  21969  opsrtoslem2  21979  evlslem4  21999  matbas2d  22326  tsmsxp  24058  ustssel  24109  ustfilxp  24116  trust  24133  restutop  24141  trcfilu  24197  cfiluweak  24198  imasdsf1olem  24277  metustfbas  24461  restmetu  24474  rrxsca  25312  madeval  27780  perpln1  28673  perpln2  28674  isperp  28675  suppovss  32637  fsuppcurry1  32681  fsuppcurry2  32682  hashxpe  32765  gsumpart  33023  gsumwrd2dccat  33033  elrgspnlem2  33193  elrgspnsubrunlem2  33198  erlval  33208  rlocval  33209  rlocbas  33217  rlocaddval  33218  rlocmulval  33219  fedgmullem1  33601  fedgmullem2  33602  fedgmul  33603  metidval  33856  esumiun  34060  filnetlem3  36353  numiunnum  36443  bj-imdirvallem  37153  bj-imdirval2  37156  bj-imdirco  37163  bj-iminvval2  37167  isrngod  37877  isgrpda  37934  iscringd  37977  aks6d1c6lem2  42144  evlsevl  42544  wdom2d2  43008  unxpwdom3  43068  trclubgNEW  43591  relexpxpmin  43690  rfovd  43974  rfovcnvf1od  43977  fsovrfovd  43982  dvsinax  45895  sge0xp  46411  gpgvtx  48028  gpgiedg  48029  imasubclem1  49090  fucofvalg  49304