Theorem unexd 7704

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565  df-uni 4846

This theorem is referenced by:  sexp2  8093  sexp3  8100  mapunen  9081  sltsun1  27805  sltsun2  27806  addsproplem2  27987  addsuniflem  28018  sltmuls1  28164  sltmuls2  28165  precsexlem11  28234  suppun2  32783  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  elrgspnsubrun  33337  elrspunsn  33519  ofun  42729  tfsconcatun  43789  rclexi  44066  rtrclexlem  44067  trclubgNEW  44069  cnvrcl0  44076  dfrtrcl5  44080  iunrelexp0  44153  relexpmulg  44161  relexp01min  44164  clnbgrval  48320