Theorem xpexd 7454

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-opab 5093  df-xp 5525  df-rel 5526

This theorem is referenced by:  cnvexg  7611  cofunexg  7632  oprabexd  7658  ofmresex  7668  opabex2  7737  offval22  7766  tposexg  7889  marypha1  8882  wdom2d  9028  ixpiunwdom  9038  fnct  9948  fpwwe2lem2  10043  fpwwe2lem5  10045  fpwwe2lem12  10052  fpwwelem  10056  canthwe  10062  pwxpndom  10077  gchhar  10090  trclexlem  14345  isacs1i  16920  brcic  17060  rescval2  17090  reschom  17092  rescabs  17095  setccofval  17334  estrccofval  17371  sylow2a  18736  lsmhash  18823  gsumxp  19089  gsumxp2  19093  opsrval  20714  opsrtoslem2  20724  evlslem4  20747  matbas2d  21028  tsmsxp  22760  ustssel  22811  ustfilxp  22818  trust  22835  restutop  22843  trcfilu  22900  cfiluweak  22901  imasdsf1olem  22980  metustfbas  23164  restmetu  23177  rrxsca  24000  perpln1  26504  perpln2  26505  isperp  26506  suppovss  30443  fsuppcurry1  30487  fsuppcurry2  30488  hashxpe  30555  gsumpart  30740  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  metidval  31243  esumiun  31463  madeval  33402  filnetlem3  33841  bj-imdirvallem  34595  bj-imdirval2  34598  bj-imdirco  34605  bj-iminvval2  34609  isrngod  35336  isgrpda  35393  iscringd  35436  wdom2d2  39976  unxpwdom3  40039  trclubgNEW  40318  relexpxpmin  40418  rfovd  40702  rfovcnvf1od  40705  fsovrfovd  40710  dvsinax  42555  sge0xp  43068