Theorem xpexd 7706

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   × cxp 5630

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 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  cnvexg  7876  fabexd  7889  cofunexg  7903  oprabexd  7929  ofmresex  7939  opabex2  8011  offval22  8040  sexp2  8098  sexp3  8105  tposexg  8192  mapunen  9086  marypha1  9349  wdom2d  9497  ixpiunwdom  9507  ttrclexg  9644  fnct  10459  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwe2lem11  10564  fpwwelem  10568  canthwe  10574  pwxpndom  10589  gchhar  10602  trclexlem  14929  isacs1i  17592  brcic  17734  rescval2  17764  reschom  17766  rescabs  17769  setccofval  18018  estrccofval  18064  sylow2a  19560  gsumxp  19917  gsumxp2  19921  opsrval  22013  opsrtoslem2  22023  evlslem4  22043  matbas2d  22379  tsmsxp  24111  ustssel  24162  ustfilxp  24169  trust  24185  restutop  24193  trcfilu  24249  cfiluweak  24250  imasdsf1olem  24329  metustfbas  24513  restmetu  24526  rrxsca  25364  madeval  27840  perpln1  28794  perpln2  28795  isperp  28796  suppovss  32770  fsuppcurry1  32813  fsuppcurry2  32814  hashxpe  32897  gsumpart  33156  gsumwrd2dccat  33171  elrgspnlem2  33336  elrgspnsubrunlem2  33341  erlval  33351  rlocval  33352  rlocbas  33360  rlocaddval  33361  rlocmulval  33362  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  metidval  34067  esumiun  34271  filnetlem3  36593  numiunnum  36683  bj-imdirvallem  37429  bj-imdirval2  37432  bj-imdirco  37439  bj-iminvval2  37443  isrngod  38143  isgrpda  38200  iscringd  38243  aks6d1c6lem2  42535  evlsevl  42926  wdom2d2  43386  unxpwdom3  43446  trclubgNEW  43968  relexpxpmin  44067  rfovd  44351  rfovcnvf1od  44354  fsovrfovd  44359  dvsinax  46265  sge0xp  46781  gpgvtx  48397  gpgiedg  48398  imasubclem1  49457  fucofvalg  49671