Theorem xpexd 7765

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  cnvexg  7936  fabexd  7949  cofunexg  7961  oprabexd  7987  ofmresex  7997  opabex2  8068  offval22  8099  sexp2  8165  sexp3  8172  tposexg  8260  mapunen  9168  marypha1  9429  wdom2d  9577  ixpiunwdom  9587  ttrclexg  9727  fnct  10623  fnctOLD  10624  fpwwe2lem2  10720  fpwwe2lem4  10722  fpwwe2lem11  10729  fpwwelem  10733  canthwe  10739  pwxpndom  10754  gchhar  10767  trclexlem  15152  isacs1i  17836  brcic  17978  rescval2  18008  reschom  18010  rescabs  18013  setccofval  18262  estrccofval  18308  sylow2a  19838  gsumxp  20195  gsumxp2  20199  opsrval  22360  opsrtoslem2  22370  evlslem4  22390  evlsevl  22446  matbas2d  22743  tsmsxp  24479  ustssel  24530  ustfilxp  24537  trust  24553  restutop  24561  trcfilu  24617  cfiluweak  24618  imasdsf1olem  24697  metustfbas  24881  restmetu  24894  rrxsca  25722  madeval  28223  perpln1  29190  perpln2  29191  isperp  29192  suppovss  33321  fsuppcurry1  33362  fsuppcurry2  33363  hashxpe  33445  gsumpart  33670  gsumwrd2dccat  33685  elrgspnlem2  33850  elrgspnsubrunlem2  33855  erlval  33865  rlocval  33866  rlocbas  33875  rlocaddval  33876  rlocmulval  33877  fedgmullem1  34307  fedgmullem2  34308  fedgmul  34309  metidval  34568  esumiun  34772  weexenwe  35812  j0ltalephlem  35946  filnetlem3  37260  numiunnum  37350  bj-imdirvallem  38194  bj-imdirval2  38197  bj-imdirco  38204  bj-iminvval2  38208  isrngod  38925  isgrpda  38982  iscringd  39025  aks6d1c6lem2  43314  wdom2d2  44135  unxpwdom3  44190  trclubgNEW  44711  relexpxpmin  44810  rfovd  45094  rfovcnvf1od  45097  fsovrfovd  45102  dvsinax  47016  sge0xp  47532  hoicvr  47651  gpgvtx  49234  gpgiedg  49235  imasubclem1  50313  fucofvalg  50533