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

Theorem unrab 3751
Description: Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
Assertion
Ref Expression
unrab  |-  ( { x  e.  A  |  ph }  u.  { x  e.  A  |  ps } )  =  {
x  e.  A  | 
( ph  \/  ps ) }

Proof of Theorem unrab
StepHypRef Expression
1 df-rab 2800 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2800 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2uneq12i 3638 . 2  |-  ( { x  e.  A  |  ph }  u.  { x  e.  A  |  ps } )  =  ( { x  |  ( x  e.  A  /\  ph ) }  u.  {
x  |  ( x  e.  A  /\  ps ) } )
4 df-rab 2800 . . 3  |-  { x  e.  A  |  ( ph  \/  ps ) }  =  { x  |  ( x  e.  A  /\  ( ph  \/  ps ) ) }
5 unab 3747 . . . 4  |-  ( { x  |  ( x  e.  A  /\  ph ) }  u.  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  A  /\  ps ) ) }
6 andi 865 . . . . 5  |-  ( ( x  e.  A  /\  ( ph  \/  ps )
)  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  A  /\  ps )
) )
76abbii 2575 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  \/  ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2473 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  u.  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  \/  ps ) ) }
94, 8eqtr4i 2473 . 2  |-  { x  e.  A  |  ( ph  \/  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  u.  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2473 1  |-  ( { x  e.  A  |  ph }  u.  { x  e.  A  |  ps } )  =  {
x  e.  A  | 
( ph  \/  ps ) }
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    /\ wa 369    = wceq 1381    e. wcel 1802   {cab 2426   {crab 2795    u. cun 3456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-un 3463
This theorem is referenced by:  rabxm  3790  kmlem3  8530  hashbclem  12475  phiprmpw  14178  efgsfo  16626  dsmmacl  18639  rrxmvallem  21697  mumul  23320  ppiub  23344  lgsquadlem2  23495  numclwwlk3lem  24973  hasheuni  27957  measvuni  28051  aean  28082  subfacp1lem6  28495  lineunray  29765  cnambfre  30031  itg2addnclem2  30035  iblabsnclem  30046  orrabdioph  30683  undisjrab  31155  mndpsuppss  32674
  Copyright terms: Public domain W3C validator