Theorem xpexd 7698

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 7697	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-opab 5149  df-xp 5630  df-rel 5631

This theorem is referenced by:  cnvexg  7868  fabexd  7881  cofunexg  7895  oprabexd  7921  ofmresex  7931  opabex2  8003  offval22  8031  sexp2  8089  sexp3  8096  tposexg  8183  mapunen  9077  marypha1  9340  wdom2d  9488  ixpiunwdom  9498  ttrclexg  9635  fnct  10450  fpwwe2lem2  10546  fpwwe2lem4  10548  fpwwe2lem11  10555  fpwwelem  10559  canthwe  10565  pwxpndom  10580  gchhar  10593  trclexlem  14947  isacs1i  17614  brcic  17756  rescval2  17786  reschom  17788  rescabs  17791  setccofval  18040  estrccofval  18086  sylow2a  19585  gsumxp  19942  gsumxp2  19946  opsrval  22034  opsrtoslem2  22044  evlslem4  22064  matbas2d  22398  tsmsxp  24130  ustssel  24181  ustfilxp  24188  trust  24204  restutop  24212  trcfilu  24268  cfiluweak  24269  imasdsf1olem  24348  metustfbas  24532  restmetu  24545  rrxsca  25373  madeval  27838  perpln1  28792  perpln2  28793  isperp  28794  suppovss  32769  fsuppcurry1  32812  fsuppcurry2  32813  hashxpe  32895  gsumpart  33139  gsumwrd2dccat  33154  elrgspnlem2  33319  elrgspnsubrunlem2  33324  erlval  33334  rlocval  33335  rlocbas  33343  rlocaddval  33344  rlocmulval  33345  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  metidval  34050  esumiun  34254  filnetlem3  36578  numiunnum  36668  bj-imdirvallem  37510  bj-imdirval2  37513  bj-imdirco  37520  bj-iminvval2  37524  isrngod  38233  isgrpda  38290  iscringd  38333  aks6d1c6lem2  42624  evlsevl  43021  wdom2d2  43481  unxpwdom3  43541  trclubgNEW  44063  relexpxpmin  44162  rfovd  44446  rfovcnvf1od  44449  fsovrfovd  44454  dvsinax  46359  sge0xp  46875  hoicvr  46994  gpgvtx  48531  gpgiedg  48532  imasubclem1  49591  fucofvalg  49805