Theorem xpexd 7730

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   × cxp 5639

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  cnvexg  7903  fabexd  7916  cofunexg  7930  oprabexd  7957  ofmresex  7967  opabex2  8039  offval22  8070  sexp2  8128  sexp3  8135  tposexg  8222  mapunen  9116  marypha1  9392  wdom2d  9540  ixpiunwdom  9550  ttrclexg  9683  fnct  10497  fpwwe2lem2  10592  fpwwe2lem4  10594  fpwwe2lem11  10601  fpwwelem  10605  canthwe  10611  pwxpndom  10626  gchhar  10639  trclexlem  14967  isacs1i  17625  brcic  17767  rescval2  17797  reschom  17799  rescabs  17802  setccofval  18051  estrccofval  18097  sylow2a  19556  gsumxp  19913  gsumxp2  19917  opsrval  21960  opsrtoslem2  21970  evlslem4  21990  matbas2d  22317  tsmsxp  24049  ustssel  24100  ustfilxp  24107  trust  24124  restutop  24132  trcfilu  24188  cfiluweak  24189  imasdsf1olem  24268  metustfbas  24452  restmetu  24465  rrxsca  25303  madeval  27767  perpln1  28644  perpln2  28645  isperp  28646  suppovss  32611  fsuppcurry1  32655  fsuppcurry2  32656  hashxpe  32739  gsumpart  33004  gsumwrd2dccat  33014  elrgspnlem2  33201  elrgspnsubrunlem2  33206  erlval  33216  rlocval  33217  rlocbas  33225  rlocaddval  33226  rlocmulval  33227  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  metidval  33887  esumiun  34091  filnetlem3  36375  numiunnum  36465  bj-imdirvallem  37175  bj-imdirval2  37178  bj-imdirco  37185  bj-iminvval2  37189  isrngod  37899  isgrpda  37956  iscringd  37999  aks6d1c6lem2  42166  evlsevl  42566  wdom2d2  43031  unxpwdom3  43091  trclubgNEW  43614  relexpxpmin  43713  rfovd  43997  rfovcnvf1od  44000  fsovrfovd  44005  dvsinax  45918  sge0xp  46434  gpgvtx  48038  gpgiedg  48039  imasubclem1  49097  fucofvalg  49311