Theorem unexd 7769

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587  df-uni 4867

This theorem is used by:  sexp2  8166  sexp3  8173  mapunen  9169  noeta2  28153  sltsun1  28180  sltsun2  28181  addsproplem2  28362  addsuniflem  28393  sltmuls1  28539  sltmuls2  28540  precsexlem11  28609  suppun2  33325  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  elrspunsn  34026  ofun  43383  tfsconcatun  44433  rclexi  44709  rtrclexlem  44710  trclubgNEW  44712  cnvrcl0  44719  dfrtrcl5  44723  iunrelexp0  44796  relexpmulg  44804  relexp01min  44807  clnbgrval  49014