Theorem xpexd 7684

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  cnvexg  7854  fabexd  7867  cofunexg  7881  oprabexd  7907  ofmresex  7917  opabex2  7989  offval22  8018  sexp2  8076  sexp3  8083  tposexg  8170  mapunen  9059  marypha1  9318  wdom2d  9466  ixpiunwdom  9476  ttrclexg  9613  fnct  10425  fpwwe2lem2  10520  fpwwe2lem4  10522  fpwwe2lem11  10529  fpwwelem  10533  canthwe  10539  pwxpndom  10554  gchhar  10567  trclexlem  14898  isacs1i  17560  brcic  17702  rescval2  17732  reschom  17734  rescabs  17737  setccofval  17986  estrccofval  18032  sylow2a  19529  gsumxp  19886  gsumxp2  19890  opsrval  21979  opsrtoslem2  21989  evlslem4  22009  matbas2d  22336  tsmsxp  24068  ustssel  24119  ustfilxp  24126  trust  24142  restutop  24150  trcfilu  24206  cfiluweak  24207  imasdsf1olem  24286  metustfbas  24470  restmetu  24483  rrxsca  25321  madeval  27791  perpln1  28686  perpln2  28687  isperp  28688  suppovss  32657  fsuppcurry1  32702  fsuppcurry2  32703  hashxpe  32784  gsumpart  33032  gsumwrd2dccat  33042  elrgspnlem2  33205  elrgspnsubrunlem2  33210  erlval  33220  rlocval  33221  rlocbas  33229  rlocaddval  33230  rlocmulval  33231  fedgmullem1  33637  fedgmullem2  33638  fedgmul  33639  metidval  33898  esumiun  34102  filnetlem3  36413  numiunnum  36503  bj-imdirvallem  37213  bj-imdirval2  37216  bj-imdirco  37223  bj-iminvval2  37227  isrngod  37937  isgrpda  37994  iscringd  38037  aks6d1c6lem2  42203  evlsevl  42603  wdom2d2  43067  unxpwdom3  43127  trclubgNEW  43650  relexpxpmin  43749  rfovd  44033  rfovcnvf1od  44036  fsovrfovd  44041  dvsinax  45950  sge0xp  46466  gpgvtx  48073  gpgiedg  48074  imasubclem1  49135  fucofvalg  49349