Theorem unexd 7708

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  sexp2  8096  sexp3  8103  sltsun1  27780  sltsun2  27781  addsproplem2  27962  addsuniflem  27993  sltmuls1  28139  sltmuls2  28140  precsexlem11  28209  suppun2  32757  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  elrspunsn  33489  ofun  42677  tfsconcatun  43765  rclexi  44042  rtrclexlem  44043  trclubgNEW  44045  cnvrcl0  44052  dfrtrcl5  44056  iunrelexp0  44129  relexpmulg  44137  relexp01min  44140  clnbgrval  48298