Theorem xpexd 7751

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-opab 5175  df-xp 5669  df-rel 5670

This theorem is referenced by:  cnvexg  7922  fabexd  7935  cofunexg  7947  oprabexd  7973  ofmresex  7983  opabex2  8055  offval22  8084  sexp2  8143  sexp3  8150  tposexg  8237  mapunen  9135  marypha1  9395  wdom2d  9543  ixpiunwdom  9553  ttrclexg  9693  fnct  10522  fpwwe2lem2  10618  fpwwe2lem4  10620  fpwwe2lem11  10627  fpwwelem  10631  canthwe  10637  pwxpndom  10652  gchhar  10665  trclexlem  15033  isacs1i  17714  brcic  17856  rescval2  17886  reschom  17888  rescabs  17891  setccofval  18140  estrccofval  18186  sylow2a  19690  gsumxp  20047  gsumxp2  20051  opsrval  22178  opsrtoslem2  22188  evlslem4  22208  evlsevl  22264  matbas2d  22561  tsmsxp  24293  ustssel  24344  ustfilxp  24351  trust  24367  restutop  24375  trcfilu  24431  cfiluweak  24432  imasdsf1olem  24511  metustfbas  24695  restmetu  24708  rrxsca  25536  madeval  28003  perpln1  28968  perpln2  28969  isperp  28970  suppovss  33004  fsuppcurry1  33047  fsuppcurry2  33048  hashxpe  33130  gsumpart  33361  gsumwrd2dccat  33376  elrgspnlem2  33541  elrgspnsubrunlem2  33546  erlval  33556  rlocval  33557  rlocbas  33566  rlocaddval  33567  rlocmulval  33568  fedgmullem1  33997  fedgmullem2  33998  fedgmul  33999  metidval  34258  esumiun  34462  filnetlem3  36869  numiunnum  36959  bj-imdirvallem  37802  bj-imdirval2  37805  bj-imdirco  37812  bj-iminvval2  37816  isrngod  38527  isgrpda  38584  iscringd  38627  aks6d1c6lem2  42916  wdom2d2  43742  unxpwdom3  43802  trclubgNEW  44324  relexpxpmin  44423  rfovd  44707  rfovcnvf1od  44710  fsovrfovd  44715  dvsinax  46607  sge0xp  47123  hoicvr  47242  gpgvtx  48785  gpgiedg  48786  imasubclem1  49859  fucofvalg  50073