Theorem xpexd 7754

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

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

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 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-rel 5658

This theorem is used by:  cnvexg  7925  fabexd  7938  cofunexg  7950  oprabexd  7976  ofmresex  7986  opabex2  8057  offval22  8088  sexp2  8147  sexp3  8154  tposexg  8241  mapunen  9149  marypha1  9410  wdom2d  9558  ixpiunwdom  9568  ttrclexg  9708  fnct  10601  fnctOLD  10602  fpwwe2lem2  10698  fpwwe2lem4  10700  fpwwe2lem11  10707  fpwwelem  10711  canthwe  10717  pwxpndom  10732  gchhar  10745  trclexlem  15127  isacs1i  17811  brcic  17953  rescval2  17983  reschom  17985  rescabs  17988  setccofval  18237  estrccofval  18283  sylow2a  19813  gsumxp  20170  gsumxp2  20174  opsrval  22335  opsrtoslem2  22345  evlslem4  22365  evlsevl  22421  matbas2d  22718  tsmsxp  24454  ustssel  24505  ustfilxp  24512  trust  24528  restutop  24536  trcfilu  24592  cfiluweak  24593  imasdsf1olem  24672  metustfbas  24856  restmetu  24869  rrxsca  25697  madeval  28200  perpln1  29167  perpln2  29168  isperp  29169  suppovss  33256  fsuppcurry1  33298  fsuppcurry2  33299  hashxpe  33381  gsumpart  33606  gsumwrd2dccat  33621  elrgspnlem2  33786  elrgspnsubrunlem2  33791  erlval  33801  rlocval  33802  rlocbas  33811  rlocaddval  33812  rlocmulval  33813  fedgmullem1  34243  fedgmullem2  34244  fedgmul  34245  metidval  34504  esumiun  34708  filnetlem3  37138  numiunnum  37228  bj-imdirvallem  38069  bj-imdirval2  38072  bj-imdirco  38079  bj-iminvval2  38083  isrngod  38800  isgrpda  38857  iscringd  38900  aks6d1c6lem2  43189  wdom2d2  43995  unxpwdom3  44055  trclubgNEW  44577  relexpxpmin  44676  rfovd  44960  rfovcnvf1od  44963  fsovrfovd  44968  dvsinax  46867  sge0xp  47383  hoicvr  47502  gpgvtx  49085  gpgiedg  49086  imasubclem1  50156  fucofvalg  50370