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

Theorem unrab 3604
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 2706 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2706 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2uneq12i 3491 . 2  |-  ( { x  e.  A  |  ph }  u.  { x  e.  A  |  ps } )  =  ( { x  |  ( x  e.  A  /\  ph ) }  u.  {
x  |  ( x  e.  A  /\  ps ) } )
4 df-rab 2706 . . 3  |-  { x  e.  A  |  ( ph  \/  ps ) }  =  { x  |  ( x  e.  A  /\  ( ph  \/  ps ) ) }
5 unab 3600 . . . 4  |-  ( { x  |  ( x  e.  A  /\  ph ) }  u.  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  A  /\  ps ) ) }
6 andi 838 . . . . 5  |-  ( ( x  e.  A  /\  ( ph  \/  ps )
)  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  A  /\  ps )
) )
76abbii 2547 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  \/  ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2458 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  u.  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  \/  ps ) ) }
94, 8eqtr4i 2458 . 2  |-  { x  e.  A  |  ( ph  \/  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  u.  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2458 1  |-  ( { x  e.  A  |  ph }  u.  { x  e.  A  |  ps } )  =  {
x  e.  A  | 
( ph  \/  ps ) }
Colors of variables: wff set class
Syntax hints:    \/ wo 358    /\ wa 359    = wceq 1652    e. wcel 1725   {cab 2421   {crab 2701    u. cun 3310
This theorem is referenced by:  rabxm  3642  kmlem3  8024  hashbclem  11693  phiprmpw  13157  efgsfo  15363  mumul  20956  ppiub  20980  lgsquadlem2  21131  hasheuni  24467  measvuni  24560  aean  24587  subfacp1lem6  24863  lineunray  26073  cnambfre  26245  itg2addnclem2  26247  iblabsnclem  26258  orrabdioph  26831  dsmmacl  27175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-un 3317
  Copyright terms: Public domain W3C validator