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 3453   × cxp 5657

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 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  cnvexg  7925  fabexd  7938  cofunexg  7950  oprabexd  7976  ofmresex  7986  opabex2  8058  offval22  8089  sexp2  8148  sexp3  8155  tposexg  8242  mapunen  9148  marypha1  9408  wdom2d  9556  ixpiunwdom  9566  ttrclexg  9706  fnct  10548  fnctOLD  10549  fpwwe2lem2  10645  fpwwe2lem4  10647  fpwwe2lem11  10654  fpwwelem  10658  canthwe  10664  pwxpndom  10679  gchhar  10692  trclexlem  15071  isacs1i  17751  brcic  17893  rescval2  17923  reschom  17925  rescabs  17928  setccofval  18177  estrccofval  18223  sylow2a  19752  gsumxp  20109  gsumxp2  20113  opsrval  22268  opsrtoslem2  22278  evlslem4  22298  evlsevl  22354  matbas2d  22651  tsmsxp  24387  ustssel  24438  ustfilxp  24445  trust  24461  restutop  24469  trcfilu  24525  cfiluweak  24526  imasdsf1olem  24605  metustfbas  24789  restmetu  24802  rrxsca  25630  madeval  28105  perpln1  29072  perpln2  29073  isperp  29074  suppovss  33161  fsuppcurry1  33203  fsuppcurry2  33204  hashxpe  33286  gsumpart  33511  gsumwrd2dccat  33526  elrgspnlem2  33691  elrgspnsubrunlem2  33696  erlval  33706  rlocval  33707  rlocbas  33716  rlocaddval  33717  rlocmulval  33718  fedgmullem1  34147  fedgmullem2  34148  fedgmul  34149  metidval  34408  esumiun  34612  filnetlem3  37007  numiunnum  37097  bj-imdirvallem  37940  bj-imdirval2  37943  bj-imdirco  37950  bj-iminvval2  37954  isrngod  38656  isgrpda  38713  iscringd  38756  aks6d1c6lem2  43045  wdom2d2  43884  unxpwdom3  43944  trclubgNEW  44466  relexpxpmin  44565  rfovd  44849  rfovcnvf1od  44852  fsovrfovd  44857  dvsinax  46749  sge0xp  47265  hoicvr  47384  gpgvtx  48967  gpgiedg  48968  imasubclem1  50038  fucofvalg  50252