Theorem unexd 7800

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4873

This theorem is used by:  sexp2  8200  sexp3  8207  mapunen  9203  noeta2  28204  sltsun1  28231  sltsun2  28232  addsproplem2  28413  addsuniflem  28444  sltmuls1  28590  sltmuls2  28591  precsexlem11  28660  suppun2  33374  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  elrspunsn  34083  ofun  43556  tfsconcatun  44600  rclexi  44876  rtrclexlem  44877  trclubgNEW  44879  cnvrcl0  44886  dfrtrcl5  44890  iunrelexp0  44963  relexpmulg  44971  relexp01min  44974  clnbgrval  49193  linply  49713