Theorem unrab 4124

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 3099	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3099	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	uneq12i 3988	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3099	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
5		unab 4120	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		andi 993	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2908	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2805	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
9	4, 8	eqtr4i 2805	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2805	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}

Syntax hints:   ∧ wa 386   ∨ wo 836   = wceq 1601   ∈ wcel 2107  {cab 2763  {crab 3094   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-un 3797

This theorem is referenced by:  rabxm  4189  kmlem3  9309  hashbclem  13550  phiprmpw  15885  efgsfo  18537  dsmmacl  20484  rrxmvallem  23610  mumul  25359  ppiub  25381  lgsquadlem2  25558  edglnl  26492  numclwwlk3lem2lem  27815  hasheuni  30745  measvuni  30875  aean  30905  subfacp1lem6  31766  lineunray  32843  cnambfre  34085  itg2addnclem2  34089  iblabsnclem  34100  orrabdioph  38309  undisjrab  39465  mndpsuppss  43171