Theorem unexd 7694

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862

This theorem is referenced by:  sexp2  8086  sexp3  8093  ssltun1  27737  ssltun2  27738  addsproplem2  27900  addsuniflem  27931  ssltmul1  28073  ssltmul2  28074  precsexlem11  28142  suppun2  32640  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrgspnsubrun  33199  elrspunsn  33376  ofun  42209  tfsconcatun  43310  rclexi  43588  rtrclexlem  43589  trclubgNEW  43591  cnvrcl0  43598  dfrtrcl5  43602  iunrelexp0  43675  relexpmulg  43683  relexp01min  43686  clnbgrval  47807