Theorem unrab 4295

Description: Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)

Assertion

Ref	Expression
unrab	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}

Proof of Theorem unrab

Step	Hyp	Ref	Expression
1		df-rab 3421	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3421	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	uneq12i 4146	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3421	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
5		unab 4288	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		andi 1009	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2803	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2762	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
9	4, 8	eqtr4i 2762	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2762	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  {cab 2714  {crab 3420   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-un 3936

This theorem is referenced by:  rabxm  4370  kmlem3  10172  hashbclem  14475  phiprmpw  16800  mndpsuppss  18748  efgsfo  19725  dsmmacl  21706  rrxmvallem  25361  mumul  27148  ppiub  27172  lgsquadlem2  27349  lrold  27865  edglnl  29127  numclwwlk3lem2lem  30369  3unrab  32489  zarclsun  33906  hasheuni  34121  measvuni  34250  aean  34280  subfacp1lem6  35212  lineunray  36170  cnambfre  37697  itg2addnclem2  37701  iblabsnclem  37712  orrabdioph  42771  sqrtcvallem1  43622  undisjrab  44297  dfsclnbgr6  47838