Theorem xpexd 7291

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

Syntax hints:   → wi 4   ∈ wcel 2050  Vcvv 3415   × cxp 5405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-opab 4992  df-xp 5413  df-rel 5414

This theorem is referenced by:  cnvexg  7444  cofunexg  7462  oprabexd  7488  ofmresex  7498  opabex2  7563  offval22  7591  tposexg  7709  marypha1  8693  wdom2d  8839  ixpiunwdom  8850  fnct  9757  fpwwe2lem2  9852  fpwwe2lem5  9854  fpwwe2lem12  9861  fpwwelem  9865  canthwe  9871  pwxpndom  9886  gchhar  9899  trclexlem  14215  isacs1i  16786  brcic  16926  rescval2  16956  reschom  16958  rescabs  16961  setccofval  17200  estrccofval  17237  sylow2a  18505  lsmhash  18589  gsumxp  18849  opsrval  19968  opsrtoslem2  19978  evlslem4  20001  matbas2d  20736  tsmsxp  22466  ustssel  22517  ustfilxp  22524  trust  22541  restutop  22549  trcfilu  22606  cfiluweak  22607  imasdsf1olem  22686  metustfbas  22870  restmetu  22883  rrxsca  23702  perpln1  26198  perpln2  26199  isperp  26200  suppovss  30187  fsuppcurry1  30220  fsuppcurry2  30221  hashxpe  30283  fedgmullem1  30660  fedgmullem2  30661  fedgmul  30662  metidval  30780  esumiun  31003  madeval  32816  filnetlem3  33255  isrngod  34624  isgrpda  34681  iscringd  34724  wdom2d2  39034  unxpwdom3  39097  trclubgNEW  39347  relexpxpmin  39431  rfovd  39716  rfovcnvf1od  39719  fsovrfovd  39724  dvsinax  41633  sge0xp  42148