MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unrab Structured version   Visualization version   GIF version

Theorem unrab 4041
Description: Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
Assertion
Ref Expression
unrab ({𝑥𝐴𝜑} ∪ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}

Proof of Theorem unrab
StepHypRef Expression
1 df-rab 3059 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 3059 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2uneq12i 3908 . 2 ({𝑥𝐴𝜑} ∪ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 3059 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 unab 4037 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐴𝜓))}
6 andi 947 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐴𝜓)))
76abbii 2877 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐴𝜓))}
85, 7eqtr4i 2785 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2785 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2785 1 ({𝑥𝐴𝜑} ∪ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wo 382  wa 383   = wceq 1632  wcel 2139  {cab 2746  {crab 3054  cun 3713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-un 3720
This theorem is referenced by:  rabxm  4104  kmlem3  9186  hashbclem  13448  phiprmpw  15703  efgsfo  18372  dsmmacl  20307  rrxmvallem  23407  mumul  25127  ppiub  25149  lgsquadlem2  25326  edglnl  26258  numclwwlk3lemOLD  27571  numclwwlk3lemlem  27572  hasheuni  30477  measvuni  30607  aean  30637  subfacp1lem6  31495  lineunray  32581  cnambfre  33789  itg2addnclem2  33793  iblabsnclem  33804  orrabdioph  37865  undisjrab  39025  mndpsuppss  42680
  Copyright terms: Public domain W3C validator