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

Theorem unrab 3853
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 2901 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 2901 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2uneq12i 3723 . 2 ({𝑥𝐴𝜑} ∪ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 2901 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 unab 3849 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐴𝜓))}
6 andi 906 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∨ (𝑥𝐴𝜓)))
76abbii 2722 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∨ (𝑥𝐴𝜓))}
85, 7eqtr4i 2631 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2631 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∪ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2631 1 ({𝑥𝐴𝜑} ∪ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wo 381  wa 382   = wceq 1474  wcel 1976  {cab 2592  {crab 2896  cun 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-un 3541
This theorem is referenced by:  rabxm  3911  kmlem3  8831  hashbclem  13042  phiprmpw  15262  efgsfo  17918  dsmmacl  19843  rrxmvallem  22909  mumul  24621  ppiub  24643  lgsquadlem2  24820  numclwwlk3lem  26398  hasheuni  29277  measvuni  29407  aean  29437  subfacp1lem6  30224  lineunray  31227  cnambfre  32428  itg2addnclem2  32432  iblabsnclem  32443  orrabdioph  36163  undisjrab  37327  av-numclwwlk3lem  41537  mndpsuppss  41945
  Copyright terms: Public domain W3C validator