Theorem unexd 7754

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593  df-uni 4874

This theorem is referenced by:  sexp2  8143  sexp3  8150  mapunen  9135  sltsun1  27962  sltsun2  27963  addsproplem2  28144  addsuniflem  28175  sltmuls1  28321  sltmuls2  28322  precsexlem11  28391  suppun2  33010  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  elrgspnsubrun  33550  elrspunsn  33718  ofun  42987  tfsconcatun  44047  rclexi  44324  rtrclexlem  44325  trclubgNEW  44327  cnvrcl0  44334  dfrtrcl5  44338  iunrelexp0  44411  relexpmulg  44419  relexp01min  44422  clnbgrval  48570