Theorem xpexd 7738

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-opab 5212  df-xp 5683  df-rel 5684

This theorem is referenced by:  cnvexg  7915  cofunexg  7935  oprabexd  7962  ofmresex  7972  opabex2  8043  offval22  8074  sexp2  8132  sexp3  8139  tposexg  8225  mapunen  9146  marypha1  9429  wdom2d  9575  ixpiunwdom  9585  ttrclexg  9718  fnct  10532  fpwwe2lem2  10627  fpwwe2lem4  10629  fpwwe2lem11  10636  fpwwelem  10640  canthwe  10646  pwxpndom  10661  gchhar  10674  trclexlem  14941  isacs1i  17601  brcic  17745  rescval2  17775  reschom  17778  rescabs  17782  rescabsOLD  17783  setccofval  18032  estrccofval  18080  sylow2a  19487  gsumxp  19844  gsumxp2  19848  opsrval  21601  opsrtoslem2  21617  evlslem4  21637  matbas2d  21925  tsmsxp  23659  ustssel  23710  ustfilxp  23717  trust  23734  restutop  23742  trcfilu  23799  cfiluweak  23800  imasdsf1olem  23879  metustfbas  24066  restmetu  24079  rrxsca  24913  madeval  27347  perpln1  27961  perpln2  27962  isperp  27963  suppovss  31906  fsuppcurry1  31950  fsuppcurry2  31951  hashxpe  32019  gsumpart  32207  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  metidval  32870  esumiun  33092  filnetlem3  35265  bj-imdirvallem  36061  bj-imdirval2  36064  bj-imdirco  36071  bj-iminvval2  36075  isrngod  36766  isgrpda  36823  iscringd  36866  evlsevl  41143  wdom2d2  41774  unxpwdom3  41837  trclubgNEW  42369  relexpxpmin  42468  rfovd  42752  rfovcnvf1od  42755  fsovrfovd  42760  dvsinax  44629  sge0xp  45145