Theorem xpexd 7758

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3461   × cxp 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-opab 5215  df-xp 5687  df-rel 5688

This theorem is referenced by:  cnvexg  7936  fabexd  7947  cofunexg  7961  oprabexd  7988  ofmresex  7998  opabex2  8070  offval22  8101  sexp2  8159  sexp3  8166  tposexg  8254  mapunen  9183  marypha1  9473  wdom2d  9619  ixpiunwdom  9629  ttrclexg  9762  fnct  10576  fpwwe2lem2  10671  fpwwe2lem4  10673  fpwwe2lem11  10680  fpwwelem  10684  canthwe  10690  pwxpndom  10705  gchhar  10718  trclexlem  14994  isacs1i  17665  brcic  17809  rescval2  17839  reschom  17842  rescabs  17846  rescabsOLD  17847  setccofval  18099  estrccofval  18147  sylow2a  19612  gsumxp  19969  gsumxp2  19973  opsrval  22045  opsrtoslem2  22061  evlslem4  22081  matbas2d  22408  tsmsxp  24142  ustssel  24193  ustfilxp  24200  trust  24217  restutop  24225  trcfilu  24282  cfiluweak  24283  imasdsf1olem  24362  metustfbas  24549  restmetu  24562  rrxsca  25407  madeval  27868  perpln1  28629  perpln2  28630  isperp  28631  suppovss  32588  fsuppcurry1  32630  fsuppcurry2  32631  hashxpe  32700  gsumpart  32901  erlval  33090  rlocval  33091  rlocbas  33099  rlocaddval  33100  rlocmulval  33101  fedgmullem1  33496  fedgmullem2  33497  fedgmul  33498  metidval  33661  esumiun  33883  filnetlem3  36040  bj-imdirvallem  36835  bj-imdirval2  36838  bj-imdirco  36845  bj-iminvval2  36849  isrngod  37547  isgrpda  37604  iscringd  37647  aks6d1c6lem2  41817  evlsevl  41985  wdom2d2  42630  unxpwdom3  42693  trclubgNEW  43222  relexpxpmin  43321  rfovd  43605  rfovcnvf1od  43608  fsovrfovd  43613  dvsinax  45471  sge0xp  45987