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

Theorem inrab 3440
Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
Assertion
Ref Expression
inrab  |-  ( { x  e.  A  |  ph }  i^i  { x  e.  A  |  ps } )  =  {
x  e.  A  | 
( ph  /\  ps ) }

Proof of Theorem inrab
StepHypRef Expression
1 df-rab 2552 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2552 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2ineq12i 3368 . 2  |-  ( { x  e.  A  |  ph }  i^i  { x  e.  A  |  ps } )  =  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  {
x  |  ( x  e.  A  /\  ps ) } )
4 df-rab 2552 . . 3  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  { x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
5 inab 3436 . . . 4  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
6 anandi 801 . . . . 5  |-  ( ( x  e.  A  /\  ( ph  /\  ps )
)  <->  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps )
) )
76abbii 2395 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  /\ 
ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2306 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
94, 8eqtr4i 2306 . 2  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2306 1  |-  ( { x  e.  A  |  ph }  i^i  { x  e.  A  |  ps } )  =  {
x  e.  A  | 
( ph  /\  ps ) }
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1623    e. wcel 1684   {cab 2269   {crab 2547    i^i cin 3151
This theorem is referenced by:  rabnc  3478  ixxin  10673  hashbclem  11390  phiprmpw  12844  submacs  14442  ablfacrp  15301  dfrhm2  15498  ordtbaslem  16918  ordtbas2  16921  ordtopn3  16926  ordtcld3  16929  ordthauslem  17111  pthaus  17332  xkohaus  17347  tsmsfbas  17810  minveclem3b  18792  shftmbl  18896  mumul  20419  ppiub  20443  lgsquadlem2  20594  xppreima  23211  xpinpreima  23290  xpinpreima2  23291  hasheuni  23453  measvuni  23542  subfacp1lem6  23716  anrabdioph  26860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator