Theorem unexd 7755

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457   ∪ cun 3904

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594  df-uni 4875

This theorem is used by:  sexp2  8144  sexp3  8151  mapunen  9137  sltsun1  28010  sltsun2  28011  addsproplem2  28192  addsuniflem  28223  sltmuls1  28369  sltmuls2  28370  precsexlem11  28439  suppun2  33058  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  elrgspnsubrun  33592  elrspunsn  33760  ofun  43039  tfsconcatun  44097  rclexi  44374  rtrclexlem  44375  trclubgNEW  44377  cnvrcl0  44384  dfrtrcl5  44388  iunrelexp0  44461  relexpmulg  44469  relexp01min  44472  clnbgrval  48620