Theorem xpexd 7687

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   × cxp 5617

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-opab 5155  df-xp 5625  df-rel 5626

This theorem is referenced by:  cnvexg  7857  fabexd  7870  cofunexg  7884  oprabexd  7910  ofmresex  7920  opabex2  7992  offval22  8021  sexp2  8079  sexp3  8086  tposexg  8173  mapunen  9063  marypha1  9324  wdom2d  9472  ixpiunwdom  9482  ttrclexg  9619  fnct  10431  fpwwe2lem2  10526  fpwwe2lem4  10528  fpwwe2lem11  10535  fpwwelem  10539  canthwe  10545  pwxpndom  10560  gchhar  10573  trclexlem  14901  isacs1i  17563  brcic  17705  rescval2  17735  reschom  17737  rescabs  17740  setccofval  17989  estrccofval  18035  sylow2a  19498  gsumxp  19855  gsumxp2  19859  opsrval  21951  opsrtoslem2  21961  evlslem4  21981  matbas2d  22308  tsmsxp  24040  ustssel  24091  ustfilxp  24098  trust  24115  restutop  24123  trcfilu  24179  cfiluweak  24180  imasdsf1olem  24259  metustfbas  24443  restmetu  24456  rrxsca  25294  madeval  27764  perpln1  28659  perpln2  28660  isperp  28661  suppovss  32631  fsuppcurry1  32676  fsuppcurry2  32677  hashxpe  32761  gsumpart  33019  gsumwrd2dccat  33029  elrgspnlem2  33192  elrgspnsubrunlem2  33197  erlval  33207  rlocval  33208  rlocbas  33216  rlocaddval  33217  rlocmulval  33218  fedgmullem1  33612  fedgmullem2  33613  fedgmul  33614  metidval  33873  esumiun  34077  filnetlem3  36374  numiunnum  36464  bj-imdirvallem  37174  bj-imdirval2  37177  bj-imdirco  37184  bj-iminvval2  37188  isrngod  37898  isgrpda  37955  iscringd  37998  aks6d1c6lem2  42164  evlsevl  42564  wdom2d2  43028  unxpwdom3  43088  trclubgNEW  43611  relexpxpmin  43710  rfovd  43994  rfovcnvf1od  43997  fsovrfovd  44002  dvsinax  45914  sge0xp  46430  gpgvtx  48047  gpgiedg  48048  imasubclem1  49109  fucofvalg  49323