Theorem xpexd 7771

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  cnvexg  7946  fabexd  7959  cofunexg  7973  oprabexd  8000  ofmresex  8010  opabex2  8082  offval22  8113  sexp2  8171  sexp3  8178  tposexg  8265  mapunen  9186  marypha1  9474  wdom2d  9620  ixpiunwdom  9630  ttrclexg  9763  fnct  10577  fpwwe2lem2  10672  fpwwe2lem4  10674  fpwwe2lem11  10681  fpwwelem  10685  canthwe  10691  pwxpndom  10706  gchhar  10719  trclexlem  15033  isacs1i  17700  brcic  17842  rescval2  17872  reschom  17874  rescabs  17877  rescabsOLD  17878  setccofval  18127  estrccofval  18173  sylow2a  19637  gsumxp  19994  gsumxp2  19998  opsrval  22064  opsrtoslem2  22080  evlslem4  22100  matbas2d  22429  tsmsxp  24163  ustssel  24214  ustfilxp  24221  trust  24238  restutop  24246  trcfilu  24303  cfiluweak  24304  imasdsf1olem  24383  metustfbas  24570  restmetu  24583  rrxsca  25430  madeval  27891  perpln1  28718  perpln2  28719  isperp  28720  suppovss  32690  fsuppcurry1  32736  fsuppcurry2  32737  hashxpe  32811  gsumpart  33060  gsumwrd2dccat  33070  elrgspnlem2  33247  elrgspnsubrunlem2  33252  erlval  33262  rlocval  33263  rlocbas  33271  rlocaddval  33272  rlocmulval  33273  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  metidval  33889  esumiun  34095  filnetlem3  36381  numiunnum  36471  bj-imdirvallem  37181  bj-imdirval2  37184  bj-imdirco  37191  bj-iminvval2  37195  isrngod  37905  isgrpda  37962  iscringd  38005  aks6d1c6lem2  42172  evlsevl  42581  wdom2d2  43047  unxpwdom3  43107  trclubgNEW  43631  relexpxpmin  43730  rfovd  44014  rfovcnvf1od  44017  fsovrfovd  44022  dvsinax  45928  sge0xp  46444  gpgvtx  48002  gpgiedg  48003  fucofvalg  49013