Theorem xpexd 7727

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  cnvexg  7900  fabexd  7913  cofunexg  7927  oprabexd  7954  ofmresex  7964  opabex2  8036  offval22  8067  sexp2  8125  sexp3  8132  tposexg  8219  mapunen  9110  marypha1  9385  wdom2d  9533  ixpiunwdom  9543  ttrclexg  9676  fnct  10490  fpwwe2lem2  10585  fpwwe2lem4  10587  fpwwe2lem11  10594  fpwwelem  10598  canthwe  10604  pwxpndom  10619  gchhar  10632  trclexlem  14960  isacs1i  17618  brcic  17760  rescval2  17790  reschom  17792  rescabs  17795  setccofval  18044  estrccofval  18090  sylow2a  19549  gsumxp  19906  gsumxp2  19910  opsrval  21953  opsrtoslem2  21963  evlslem4  21983  matbas2d  22310  tsmsxp  24042  ustssel  24093  ustfilxp  24100  trust  24117  restutop  24125  trcfilu  24181  cfiluweak  24182  imasdsf1olem  24261  metustfbas  24445  restmetu  24458  rrxsca  25296  madeval  27760  perpln1  28637  perpln2  28638  isperp  28639  suppovss  32604  fsuppcurry1  32648  fsuppcurry2  32649  hashxpe  32732  gsumpart  32997  gsumwrd2dccat  33007  elrgspnlem2  33194  elrgspnsubrunlem2  33199  erlval  33209  rlocval  33210  rlocbas  33218  rlocaddval  33219  rlocmulval  33220  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  metidval  33880  esumiun  34084  filnetlem3  36368  numiunnum  36458  bj-imdirvallem  37168  bj-imdirval2  37171  bj-imdirco  37178  bj-iminvval2  37182  isrngod  37892  isgrpda  37949  iscringd  37992  aks6d1c6lem2  42159  evlsevl  42559  wdom2d2  43024  unxpwdom3  43084  trclubgNEW  43607  relexpxpmin  43706  rfovd  43990  rfovcnvf1od  43993  fsovrfovd  43998  dvsinax  45911  sge0xp  46427  gpgvtx  48034  gpgiedg  48035  imasubclem1  49093  fucofvalg  49307