Theorem xpexd 7769

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  cnvexg  7946  fabexd  7957  cofunexg  7971  oprabexd  7998  ofmresex  8008  opabex2  8080  offval22  8111  sexp2  8169  sexp3  8176  tposexg  8263  mapunen  9184  marypha1  9471  wdom2d  9617  ixpiunwdom  9627  ttrclexg  9760  fnct  10574  fpwwe2lem2  10669  fpwwe2lem4  10671  fpwwe2lem11  10678  fpwwelem  10682  canthwe  10688  pwxpndom  10703  gchhar  10716  trclexlem  15029  isacs1i  17701  brcic  17845  rescval2  17875  reschom  17878  rescabs  17882  rescabsOLD  17883  setccofval  18135  estrccofval  18183  sylow2a  19651  gsumxp  20008  gsumxp2  20012  opsrval  22081  opsrtoslem2  22097  evlslem4  22117  matbas2d  22444  tsmsxp  24178  ustssel  24229  ustfilxp  24236  trust  24253  restutop  24261  trcfilu  24318  cfiluweak  24319  imasdsf1olem  24398  metustfbas  24585  restmetu  24598  rrxsca  25443  madeval  27905  perpln1  28732  perpln2  28733  isperp  28734  suppovss  32695  fsuppcurry1  32742  fsuppcurry2  32743  hashxpe  32816  gsumpart  33042  gsumwrd2dccat  33052  elrgspnlem2  33232  erlval  33244  rlocval  33245  rlocbas  33253  rlocaddval  33254  rlocmulval  33255  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  metidval  33850  esumiun  34074  filnetlem3  36362  numiunnum  36452  bj-imdirvallem  37162  bj-imdirval2  37165  bj-imdirco  37172  bj-iminvval2  37176  isrngod  37884  isgrpda  37941  iscringd  37984  aks6d1c6lem2  42152  evlsevl  42557  wdom2d2  43023  unxpwdom3  43083  trclubgNEW  43607  relexpxpmin  43706  rfovd  43990  rfovcnvf1od  43993  fsovrfovd  43998  dvsinax  45868  sge0xp  46384  gpgvtx  47937  gpgiedg  47938