MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unexd Structured version   Visualization version   GIF version

Theorem unexd 7773
Description: The union of two sets is a set. (Contributed by SN, 16-Jul-2024.)
Hypotheses
Ref Expression
unexd.1 (𝜑𝐴𝑉)
unexd.2 (𝜑𝐵𝑊)
Assertion
Ref Expression
unexd (𝜑 → (𝐴𝐵) ∈ V)

Proof of Theorem unexd
StepHypRef Expression
1 unexd.1 . 2 (𝜑𝐴𝑉)
2 unexd.2 . 2 (𝜑𝐵𝑊)
3 unexg 7762 . 2 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Vcvv 3478  cun 3961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-sn 4632  df-pr 4634  df-uni 4913
This theorem is referenced by:  sexp2  8170  sexp3  8177  ssltun1  27868  ssltun2  27869  addsproplem2  28018  addsuniflem  28049  ssltmul1  28188  ssltmul2  28189  precsexlem11  28256  suppun2  32699  elrspunsn  33437  ofun  42256  tfsconcatun  43327  rclexi  43605  rtrclexlem  43606  trclubgNEW  43608  cnvrcl0  43615  dfrtrcl5  43619  iunrelexp0  43692  relexpmulg  43700  relexp01min  43703  clnbgrval  47747
  Copyright terms: Public domain W3C validator