Theorem unexd 7756

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3471   ∪ cun 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4909

This theorem is referenced by:  sexp2  8151  sexp3  8158  ssltun1  27754  ssltun2  27755  addsproplem2  27900  addsuniflem  27931  ssltmul1  28060  ssltmul2  28061  precsexlem11  28128  elrspunsn  33158  ofun  41727  tfsconcatun  42766  rclexi  43045  rtrclexlem  43046  trclubgNEW  43048  cnvrcl0  43055  dfrtrcl5  43059  iunrelexp0  43132  relexpmulg  43140  relexp01min  43143

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »