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

Theorem inrab 3613
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 2714 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2714 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2ineq12i 3540 . 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 2714 . . 3  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  { x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
5 inab 3609 . . . 4  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
6 anandi 802 . . . . 5  |-  ( ( x  e.  A  /\  ( ph  /\  ps )
)  <->  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps )
) )
76abbii 2548 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  /\ 
ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2459 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
94, 8eqtr4i 2459 . 2  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2459 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 359    = wceq 1652    e. wcel 1725   {cab 2422   {crab 2709    i^i cin 3319
This theorem is referenced by:  rabnc  3651  ixxin  10933  hashbclem  11701  phiprmpw  13165  submacs  14765  ablfacrp  15624  dfrhm2  15821  ordtbaslem  17252  ordtbas2  17255  ordtopn3  17260  ordtcld3  17263  ordthauslem  17447  pthaus  17670  xkohaus  17685  tsmsfbas  18157  minveclem3b  19329  shftmbl  19433  mumul  20964  ppiub  20988  lgsquadlem2  21139  cusgrasizeindslem2  21483  xppreima  24059  xpinpreima  24304  xpinpreima2  24305  measvuni  24568  subfacp1lem6  24871  cnambfre  26255  itg2addnclem2  26257  ftc1anclem6  26285  anrabdioph  26839  frisusgranb  28387
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-in 3327
  Copyright terms: Public domain W3C validator