Theorem xpexd 7750

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-opab 5168  df-xp 5661  df-rel 5662

This theorem is used by:  cnvexg  7921  fabexd  7934  cofunexg  7946  oprabexd  7972  ofmresex  7982  opabex2  8054  offval22  8085  sexp2  8144  sexp3  8151  tposexg  8238  mapunen  9144  marypha1  9404  wdom2d  9552  ixpiunwdom  9562  ttrclexg  9702  fnct  10544  fnctOLD  10545  fpwwe2lem2  10641  fpwwe2lem4  10643  fpwwe2lem11  10650  fpwwelem  10654  canthwe  10660  pwxpndom  10675  gchhar  10688  trclexlem  15067  isacs1i  17745  brcic  17887  rescval2  17917  reschom  17919  rescabs  17922  setccofval  18171  estrccofval  18217  sylow2a  19746  gsumxp  20103  gsumxp2  20107  opsrval  22262  opsrtoslem2  22272  evlslem4  22292  evlsevl  22348  matbas2d  22645  tsmsxp  24381  ustssel  24432  ustfilxp  24439  trust  24455  restutop  24463  trcfilu  24519  cfiluweak  24520  imasdsf1olem  24599  metustfbas  24783  restmetu  24796  rrxsca  25624  madeval  28097  perpln1  29064  perpln2  29065  isperp  29066  suppovss  33153  fsuppcurry1  33195  fsuppcurry2  33196  hashxpe  33278  gsumpart  33503  gsumwrd2dccat  33518  elrgspnlem2  33683  elrgspnsubrunlem2  33688  erlval  33698  rlocval  33699  rlocbas  33708  rlocaddval  33709  rlocmulval  33710  fedgmullem1  34139  fedgmullem2  34140  fedgmul  34141  metidval  34400  esumiun  34604  filnetlem3  36999  numiunnum  37089  bj-imdirvallem  37932  bj-imdirval2  37935  bj-imdirco  37942  bj-iminvval2  37946  isrngod  38648  isgrpda  38705  iscringd  38748  aks6d1c6lem2  43037  wdom2d2  43876  unxpwdom3  43936  trclubgNEW  44458  relexpxpmin  44557  rfovd  44841  rfovcnvf1od  44844  fsovrfovd  44849  dvsinax  46741  sge0xp  47257  hoicvr  47376  gpgvtx  48959  gpgiedg  48960  imasubclem1  50030  fucofvalg  50244