Theorem unexd 7731

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

Step	Hyp	Ref	Expression
1		unexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		unexd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		unexg 7720	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919  df-sn 4580  df-pr 4582  df-uni 4863

This theorem is referenced by:  sexp2  8119  sexp3  8126  mapunen  9111  sltsun1  27868  sltsun2  27869  addsproplem2  28050  addsuniflem  28081  sltmuls1  28227  sltmuls2  28228  precsexlem11  28297  suppun2  32846  elrgspnsubrunlem1  33388  elrgspnsubrunlem2  33389  elrgspnsubrun  33390  elrspunsn  33575  ofun  42814  tfsconcatun  43874  rclexi  44151  rtrclexlem  44152  trclubgNEW  44154  cnvrcl0  44161  dfrtrcl5  44165  iunrelexp0  44238  relexpmulg  44246  relexp01min  44249  clnbgrval  48404