Theorem xpexd 7730

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-opab 5162  df-xp 5651  df-rel 5652

This theorem is referenced by:  cnvexg  7901  fabexd  7914  cofunexg  7926  oprabexd  7952  ofmresex  7962  opabex2  8034  offval22  8062  sexp2  8121  sexp3  8128  tposexg  8215  mapunen  9114  marypha1  9377  wdom2d  9525  ixpiunwdom  9535  ttrclexg  9675  fnct  10491  fpwwe2lem2  10587  fpwwe2lem4  10589  fpwwe2lem11  10596  fpwwelem  10600  canthwe  10606  pwxpndom  10621  gchhar  10634  trclexlem  15004  isacs1i  17672  brcic  17814  rescval2  17844  reschom  17846  rescabs  17849  setccofval  18098  estrccofval  18144  sylow2a  19642  gsumxp  19999  gsumxp2  20003  opsrval  22079  opsrtoslem2  22089  evlslem4  22109  evlsevl  22165  matbas2d  22463  tsmsxp  24195  ustssel  24246  ustfilxp  24253  trust  24269  restutop  24277  trcfilu  24333  cfiluweak  24334  imasdsf1olem  24413  metustfbas  24597  restmetu  24610  rrxsca  25438  madeval  27902  perpln1  28856  perpln2  28857  isperp  28858  suppovss  32833  fsuppcurry1  32876  fsuppcurry2  32877  hashxpe  32959  gsumpart  33204  gsumwrd2dccat  33219  elrgspnlem2  33385  elrgspnsubrunlem2  33390  erlval  33400  rlocval  33401  rlocbas  33410  rlocaddval  33411  rlocmulval  33412  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  metidval  34148  esumiun  34352  filnetlem3  36704  numiunnum  36794  bj-imdirvallem  37636  bj-imdirval2  37639  bj-imdirco  37646  bj-iminvval2  37650  isrngod  38361  isgrpda  38418  iscringd  38461  aks6d1c6lem2  42752  wdom2d2  43576  unxpwdom3  43636  trclubgNEW  44158  relexpxpmin  44257  rfovd  44541  rfovcnvf1od  44544  fsovrfovd  44549  dvsinax  46451  sge0xp  46967  hoicvr  47086  gpgvtx  48629  gpgiedg  48630  imasubclem1  49689  fucofvalg  49903