Theorem xpexd 7595

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3431   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-opab 5142  df-xp 5596  df-rel 5597

This theorem is referenced by:  cnvexg  7765  cofunexg  7785  oprabexd  7811  ofmresex  7821  opabex2  7890  offval22  7919  tposexg  8047  mapunen  8915  marypha1  9171  wdom2d  9317  ixpiunwdom  9327  ttrclexg  9459  fnct  10294  fpwwe2lem2  10389  fpwwe2lem4  10391  fpwwe2lem11  10398  fpwwelem  10402  canthwe  10408  pwxpndom  10423  gchhar  10436  trclexlem  14703  isacs1i  17364  brcic  17508  rescval2  17538  reschom  17541  rescabs  17545  rescabsOLD  17546  setccofval  17795  estrccofval  17843  sylow2a  19222  gsumxp  19575  gsumxp2  19579  opsrval  21245  opsrtoslem2  21261  evlslem4  21282  matbas2d  21570  tsmsxp  23304  ustssel  23355  ustfilxp  23362  trust  23379  restutop  23387  trcfilu  23444  cfiluweak  23445  imasdsf1olem  23524  metustfbas  23711  restmetu  23724  rrxsca  24558  perpln1  27069  perpln2  27070  isperp  27071  suppovss  31013  fsuppcurry1  31056  fsuppcurry2  31057  hashxpe  31123  gsumpart  31311  fedgmullem1  31706  fedgmullem2  31707  fedgmul  31708  metidval  31836  esumiun  32058  sexp2  33789  sexp3  33795  madeval  34032  filnetlem3  34565  bj-imdirvallem  35347  bj-imdirval2  35350  bj-imdirco  35357  bj-iminvval2  35361  isrngod  36052  isgrpda  36109  iscringd  36152  evlsbagval  40272  wdom2d2  40854  unxpwdom3  40917  trclubgNEW  41196  relexpxpmin  41295  rfovd  41579  rfovcnvf1od  41582  fsovrfovd  41587  dvsinax  43425  sge0xp  43938