Theorem xpexd 7738

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

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3457   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-opab 5168  df-xp 5658  df-rel 5659

This theorem is referenced by:  cnvexg  7909  fabexd  7922  cofunexg  7934  oprabexd  7960  ofmresex  7970  opabex2  8042  offval22  8071  sexp2  8130  sexp3  8137  tposexg  8224  mapunen  9122  marypha1  9382  wdom2d  9530  ixpiunwdom  9540  ttrclexg  9680  fnct  10509  fpwwe2lem2  10605  fpwwe2lem4  10607  fpwwe2lem11  10614  fpwwelem  10618  canthwe  10624  pwxpndom  10639  gchhar  10652  trclexlem  15021  isacs1i  17703  brcic  17845  rescval2  17875  reschom  17877  rescabs  17880  setccofval  18129  estrccofval  18175  sylow2a  19680  gsumxp  20037  gsumxp2  20041  opsrval  22157  opsrtoslem2  22167  evlslem4  22187  evlsevl  22243  matbas2d  22541  tsmsxp  24273  ustssel  24324  ustfilxp  24331  trust  24347  restutop  24355  trcfilu  24411  cfiluweak  24412  imasdsf1olem  24491  metustfbas  24675  restmetu  24688  rrxsca  25516  madeval  27983  perpln1  28941  perpln2  28942  isperp  28943  suppovss  32938  fsuppcurry1  32981  fsuppcurry2  32982  hashxpe  33064  gsumpart  33296  gsumwrd2dccat  33311  elrgspnlem2  33476  elrgspnsubrunlem2  33481  erlval  33491  rlocval  33492  rlocbas  33501  rlocaddval  33502  rlocmulval  33503  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  metidval  34197  esumiun  34401  filnetlem3  36753  numiunnum  36843  bj-imdirvallem  37684  bj-imdirval2  37687  bj-imdirco  37694  bj-iminvval2  37698  isrngod  38409  isgrpda  38466  iscringd  38509  aks6d1c6lem2  42800  wdom2d2  43624  unxpwdom3  43684  trclubgNEW  44206  relexpxpmin  44305  rfovd  44589  rfovcnvf1od  44592  fsovrfovd  44597  dvsinax  46485  sge0xp  47001  hoicvr  47120  gpgvtx  48663  gpgiedg  48664  imasubclem1  49733  fucofvalg  49947