Theorem xpexd 7792

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   × cxp 5654

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332  ax-pr 5396  ax-un 7778

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-opab 5172  df-xp 5662  df-rel 5663

This theorem is used by:  cnvexg  7963  fabexd  7976  cofunexg  7988  oprabexd  8014  ofmresex  8024  opabex2  8096  offval22  8127  sexp2  8193  sexp3  8200  tposexg  8288  mapunen  9196  marypha1  9456  wdom2d  9604  ixpiunwdom  9614  ttrclexg  9754  fnct  10650  fnctOLD  10651  fpwwe2lem2  10747  fpwwe2lem4  10749  fpwwe2lem11  10756  fpwwelem  10760  canthwe  10766  pwxpndom  10781  gchhar  10794  trclexlem  15179  isacs1i  17863  brcic  18005  rescval2  18035  reschom  18037  rescabs  18040  setccofval  18289  estrccofval  18335  sylow2a  19866  gsumxp  20223  gsumxp2  20227  opsrval  22388  opsrtoslem2  22398  evlslem4  22418  evlsevl  22474  matbas2d  22771  tsmsxp  24507  ustssel  24558  ustfilxp  24565  trust  24581  restutop  24589  trcfilu  24645  cfiluweak  24646  imasdsf1olem  24725  metustfbas  24909  restmetu  24922  rrxsca  25750  madeval  28251  perpln1  29218  perpln2  29219  isperp  29220  suppovss  33348  fsuppcurry1  33389  fsuppcurry2  33390  hashxpe  33472  gsumpart  33700  gsumwrd2dccat  33715  elrgspnlem2  33880  elrgspnsubrunlem2  33885  erlval  33895  rlocval  33896  rlocbas  33905  rlocaddval  33906  rlocmulval  33907  fedgmullem1  34344  fedgmullem2  34345  fedgmul  34346  metidval  34605  esumiun  34809  weexenwe  35861  j0ltalephlem  36020  filnetlem3  37359  numiunnum  37449  bj-imdirvallem  38306  bj-imdirval2  38309  bj-imdirco  38316  bj-iminvval2  38320  isrngod  39035  isgrpda  39092  iscringd  39135  aks6d1c6lem2  43424  wdom2d2  44246  unxpwdom3  44301  trclubgNEW  44821  relexpxpmin  44920  rfovd  45204  rfovcnvf1od  45207  fsovrfovd  45212  dvsinax  47138  sge0xp  47654  hoicvr  47773  gpgvtx  49356  gpgiedg  49357  imasubclem1  50435  fucofvalg  50655