Theorem xpexd 7734

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   × cxp 5673

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-opab 5210  df-xp 5681  df-rel 5682

This theorem is referenced by:  cnvexg  7911  cofunexg  7931  oprabexd  7958  ofmresex  7968  opabex2  8039  offval22  8070  sexp2  8128  sexp3  8135  tposexg  8221  mapunen  9142  marypha1  9425  wdom2d  9571  ixpiunwdom  9581  ttrclexg  9714  fnct  10528  fpwwe2lem2  10623  fpwwe2lem4  10625  fpwwe2lem11  10632  fpwwelem  10636  canthwe  10642  pwxpndom  10657  gchhar  10670  trclexlem  14937  isacs1i  17597  brcic  17741  rescval2  17771  reschom  17774  rescabs  17778  rescabsOLD  17779  setccofval  18028  estrccofval  18076  sylow2a  19481  gsumxp  19838  gsumxp2  19842  opsrval  21592  opsrtoslem2  21608  evlslem4  21628  matbas2d  21916  tsmsxp  23650  ustssel  23701  ustfilxp  23708  trust  23725  restutop  23733  trcfilu  23790  cfiluweak  23791  imasdsf1olem  23870  metustfbas  24057  restmetu  24070  rrxsca  24904  madeval  27336  perpln1  27950  perpln2  27951  isperp  27952  suppovss  31893  fsuppcurry1  31937  fsuppcurry2  31938  hashxpe  32006  gsumpart  32194  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  metidval  32858  esumiun  33080  filnetlem3  35253  bj-imdirvallem  36049  bj-imdirval2  36052  bj-imdirco  36059  bj-iminvval2  36063  isrngod  36754  isgrpda  36811  iscringd  36854  evlsevl  41140  wdom2d2  41759  unxpwdom3  41822  trclubgNEW  42354  relexpxpmin  42453  rfovd  42737  rfovcnvf1od  42740  fsovrfovd  42745  dvsinax  44615  sge0xp  45131