Theorem xpexd 7759

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  cnvexg  7930  fabexd  7943  cofunexg  7955  oprabexd  7981  ofmresex  7991  opabex2  8063  offval22  8092  sexp2  8151  sexp3  8158  tposexg  8245  mapunen  9144  marypha1  9404  wdom2d  9552  ixpiunwdom  9562  ttrclexg  9702  fnct  10539  fpwwe2lem2  10635  fpwwe2lem4  10637  fpwwe2lem11  10644  fpwwelem  10648  canthwe  10654  pwxpndom  10669  gchhar  10682  trclexlem  15057  isacs1i  17738  brcic  17880  rescval2  17910  reschom  17912  rescabs  17915  setccofval  18164  estrccofval  18210  sylow2a  19720  gsumxp  20077  gsumxp2  20081  opsrval  22234  opsrtoslem2  22244  evlslem4  22264  evlsevl  22320  matbas2d  22617  tsmsxp  24349  ustssel  24400  ustfilxp  24407  trust  24423  restutop  24431  trcfilu  24487  cfiluweak  24488  imasdsf1olem  24567  metustfbas  24751  restmetu  24764  rrxsca  25592  madeval  28062  perpln1  29027  perpln2  29028  isperp  29029  suppovss  33063  fsuppcurry1  33106  fsuppcurry2  33107  hashxpe  33189  gsumpart  33414  gsumwrd2dccat  33429  elrgspnlem2  33594  elrgspnsubrunlem2  33599  erlval  33609  rlocval  33610  rlocbas  33619  rlocaddval  33620  rlocmulval  33621  fedgmullem1  34050  fedgmullem2  34051  fedgmul  34052  metidval  34311  esumiun  34515  filnetlem3  36931  numiunnum  37021  bj-imdirvallem  37864  bj-imdirval2  37867  bj-imdirco  37874  bj-iminvval2  37878  isrngod  38589  isgrpda  38646  iscringd  38689  aks6d1c6lem2  42978  wdom2d2  43802  unxpwdom3  43862  trclubgNEW  44384  relexpxpmin  44483  rfovd  44767  rfovcnvf1od  44770  fsovrfovd  44775  dvsinax  46667  sge0xp  47183  hoicvr  47302  gpgvtx  48848  gpgiedg  48849  imasubclem1  49922  fucofvalg  50136