Theorem xpexd 7745

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   × cxp 5652

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  cnvexg  7920  fabexd  7933  cofunexg  7947  oprabexd  7974  ofmresex  7984  opabex2  8056  offval22  8087  sexp2  8145  sexp3  8152  tposexg  8239  mapunen  9160  marypha1  9446  wdom2d  9594  ixpiunwdom  9604  ttrclexg  9737  fnct  10551  fpwwe2lem2  10646  fpwwe2lem4  10648  fpwwe2lem11  10655  fpwwelem  10659  canthwe  10665  pwxpndom  10680  gchhar  10693  trclexlem  15013  isacs1i  17669  brcic  17811  rescval2  17841  reschom  17843  rescabs  17846  setccofval  18095  estrccofval  18141  sylow2a  19600  gsumxp  19957  gsumxp2  19961  opsrval  22004  opsrtoslem2  22014  evlslem4  22034  matbas2d  22361  tsmsxp  24093  ustssel  24144  ustfilxp  24151  trust  24168  restutop  24176  trcfilu  24232  cfiluweak  24233  imasdsf1olem  24312  metustfbas  24496  restmetu  24509  rrxsca  25348  madeval  27812  perpln1  28689  perpln2  28690  isperp  28691  suppovss  32658  fsuppcurry1  32702  fsuppcurry2  32703  hashxpe  32786  gsumpart  33051  gsumwrd2dccat  33061  elrgspnlem2  33238  elrgspnsubrunlem2  33243  erlval  33253  rlocval  33254  rlocbas  33262  rlocaddval  33263  rlocmulval  33264  fedgmullem1  33669  fedgmullem2  33670  fedgmul  33671  metidval  33921  esumiun  34125  filnetlem3  36398  numiunnum  36488  bj-imdirvallem  37198  bj-imdirval2  37201  bj-imdirco  37208  bj-iminvval2  37212  isrngod  37922  isgrpda  37979  iscringd  38022  aks6d1c6lem2  42184  evlsevl  42594  wdom2d2  43059  unxpwdom3  43119  trclubgNEW  43642  relexpxpmin  43741  rfovd  44025  rfovcnvf1od  44028  fsovrfovd  44033  dvsinax  45942  sge0xp  46458  gpgvtx  48047  gpgiedg  48048  imasubclem1  49063  fucofvalg  49229