Theorem unrab 4267

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 3400	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3400	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	uneq12i 4118	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3400	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
5		unab 4260	. . . 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 1541   ∈ wcel 2113  {cab 2714  {crab 3399   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906

This theorem is referenced by:  rabxm  4342  kmlem3  10063  hashbclem  14375  phiprmpw  16703  mndpsuppss  18690  efgsfo  19668  dsmmacl  21696  rrxmvallem  25360  mumul  27147  ppiub  27171  lgsquadlem2  27348  lrold  27893  edglnl  29216  numclwwlk3lem2lem  30458  3unrab  32578  zarclsun  34027  hasheuni  34242  measvuni  34371  aean  34401  subfacp1lem6  35379  lineunray  36341  cnambfre  37869  itg2addnclem2  37873  iblabsnclem  37884  orrabdioph  43023  sqrtcvallem1  43872  undisjrab  44547  dfsclnbgr6  48104