Theorem xpexd 7701

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  cnvexg  7871  fabexd  7884  cofunexg  7898  oprabexd  7924  ofmresex  7934  opabex2  8006  offval22  8034  sexp2  8093  sexp3  8100  tposexg  8187  mapunen  9081  marypha1  9344  wdom2d  9492  ixpiunwdom  9502  ttrclexg  9642  fnct  10457  fpwwe2lem2  10553  fpwwe2lem4  10555  fpwwe2lem11  10562  fpwwelem  10566  canthwe  10572  pwxpndom  10587  gchhar  10600  trclexlem  14954  isacs1i  17621  brcic  17763  rescval2  17793  reschom  17795  rescabs  17798  setccofval  18047  estrccofval  18093  sylow2a  19592  gsumxp  19949  gsumxp2  19953  opsrval  22029  opsrtoslem2  22039  evlslem4  22059  evlsevl  22115  matbas2d  22413  tsmsxp  24145  ustssel  24196  ustfilxp  24203  trust  24219  restutop  24227  trcfilu  24283  cfiluweak  24284  imasdsf1olem  24363  metustfbas  24547  restmetu  24560  rrxsca  25388  madeval  27849  perpln1  28803  perpln2  28804  isperp  28805  suppovss  32780  fsuppcurry1  32823  fsuppcurry2  32824  hashxpe  32906  gsumpart  33151  gsumwrd2dccat  33166  elrgspnlem2  33331  elrgspnsubrunlem2  33336  erlval  33346  rlocval  33347  rlocbas  33355  rlocaddval  33356  rlocmulval  33357  fedgmullem1  33820  fedgmullem2  33821  fedgmul  33822  metidval  34081  esumiun  34285  filnetlem3  36615  numiunnum  36705  bj-imdirvallem  37547  bj-imdirval2  37550  bj-imdirco  37557  bj-iminvval2  37561  isrngod  38272  isgrpda  38329  iscringd  38372  aks6d1c6lem2  42663  wdom2d2  43487  unxpwdom3  43547  trclubgNEW  44069  relexpxpmin  44168  rfovd  44452  rfovcnvf1od  44455  fsovrfovd  44460  dvsinax  46363  sge0xp  46879  hoicvr  46998  gpgvtx  48541  gpgiedg  48542  imasubclem1  49601  fucofvalg  49815