Theorem xpexd 7705

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   × cxp 5629

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 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  cnvexg  7875  fabexd  7888  cofunexg  7902  oprabexd  7928  ofmresex  7938  opabex2  8010  offval22  8038  sexp2  8096  sexp3  8103  tposexg  8190  mapunen  9084  marypha1  9347  wdom2d  9495  ixpiunwdom  9505  ttrclexg  9644  fnct  10459  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwe2lem11  10564  fpwwelem  10568  canthwe  10574  pwxpndom  10589  gchhar  10602  trclexlem  14956  isacs1i  17623  brcic  17765  rescval2  17795  reschom  17797  rescabs  17800  setccofval  18049  estrccofval  18095  sylow2a  19594  gsumxp  19951  gsumxp2  19955  opsrval  22024  opsrtoslem2  22034  evlslem4  22054  matbas2d  22388  tsmsxp  24120  ustssel  24171  ustfilxp  24178  trust  24194  restutop  24202  trcfilu  24258  cfiluweak  24259  imasdsf1olem  24338  metustfbas  24522  restmetu  24535  rrxsca  25363  madeval  27824  perpln1  28778  perpln2  28779  isperp  28780  suppovss  32754  fsuppcurry1  32797  fsuppcurry2  32798  hashxpe  32880  gsumpart  33124  gsumwrd2dccat  33139  elrgspnlem2  33304  elrgspnsubrunlem2  33309  erlval  33319  rlocval  33320  rlocbas  33328  rlocaddval  33329  rlocmulval  33330  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  metidval  34034  esumiun  34238  filnetlem3  36562  numiunnum  36652  bj-imdirvallem  37494  bj-imdirval2  37497  bj-imdirco  37504  bj-iminvval2  37508  isrngod  38219  isgrpda  38276  iscringd  38319  aks6d1c6lem2  42610  evlsevl  43007  wdom2d2  43463  unxpwdom3  43523  trclubgNEW  44045  relexpxpmin  44144  rfovd  44428  rfovcnvf1od  44431  fsovrfovd  44436  dvsinax  46341  sge0xp  46857  hoicvr  46976  gpgvtx  48519  gpgiedg  48520  imasubclem1  49579  fucofvalg  49793