Theorem unrab 4261

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 3414	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3414	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	uneq12i 4113	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 3414	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
5		unab 4254	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		andi 1025	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2828	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2787	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∨ 𝜓))}
9	4, 8	eqtr4i 2787	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∪ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2787	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145  {cab 2739  {crab 3413   ∪ cun 3897

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 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904

This theorem is used by:  rabxm  4340  kmlem3  10231  hashbclem  14597  phiprmpw  16953  mndpsuppss  18959  efgsfo  19953  dsmmacl  22047  rrxmvallem  25725  mumul  27508  ppiub  27531  lgsquadlem2  27708  lrold  28283  edglnl  29721  numclwwlk3lem2lem  30984  3unrab  33099  zarclsun  34502  hasheuni  34717  measvuni  34847  aean  34877  subfacp1lem6  35950  lineunray  36912  cnambfre  38586  itg2addnclem2  38590  iblabsnclem  38601  orrabdioph  43791  sqrtcvallem1  44630  undisjrab  45289  dfsclnbgr6  48955