Theorem xpexd 7696

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  cnvexg  7866  fabexd  7879  cofunexg  7893  oprabexd  7919  ofmresex  7929  opabex2  8001  offval22  8030  sexp2  8088  sexp3  8095  tposexg  8182  mapunen  9074  marypha1  9337  wdom2d  9485  ixpiunwdom  9495  ttrclexg  9632  fnct  10447  fpwwe2lem2  10543  fpwwe2lem4  10545  fpwwe2lem11  10552  fpwwelem  10556  canthwe  10562  pwxpndom  10577  gchhar  10590  trclexlem  14917  isacs1i  17580  brcic  17722  rescval2  17752  reschom  17754  rescabs  17757  setccofval  18006  estrccofval  18052  sylow2a  19548  gsumxp  19905  gsumxp2  19909  opsrval  22001  opsrtoslem2  22011  evlslem4  22031  matbas2d  22367  tsmsxp  24099  ustssel  24150  ustfilxp  24157  trust  24173  restutop  24181  trcfilu  24237  cfiluweak  24238  imasdsf1olem  24317  metustfbas  24501  restmetu  24514  rrxsca  25352  madeval  27828  perpln1  28782  perpln2  28783  isperp  28784  suppovss  32760  fsuppcurry1  32803  fsuppcurry2  32804  hashxpe  32887  gsumpart  33146  gsumwrd2dccat  33160  elrgspnlem2  33325  elrgspnsubrunlem2  33330  erlval  33340  rlocval  33341  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  metidval  34047  esumiun  34251  filnetlem3  36574  numiunnum  36664  bj-imdirvallem  37381  bj-imdirval2  37384  bj-imdirco  37391  bj-iminvval2  37395  isrngod  38095  isgrpda  38152  iscringd  38195  aks6d1c6lem2  42421  evlsevl  42813  wdom2d2  43273  unxpwdom3  43333  trclubgNEW  43855  relexpxpmin  43954  rfovd  44238  rfovcnvf1od  44241  fsovrfovd  44246  dvsinax  46153  sge0xp  46669  gpgvtx  48285  gpgiedg  48286  imasubclem1  49345  fucofvalg  49559