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

Theorem inrab 3601
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 2721 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2721 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2ineq12i 3529 . 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 2721 . . 3  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  { x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
5 inab 3597 . . . 4  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
6 anandi 803 . . . . 5  |-  ( ( x  e.  A  /\  ( ph  /\  ps )
)  <->  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps )
) )
76abbii 2555 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  /\ 
ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2466 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
94, 8eqtr4i 2466 . 2  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2466 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 360    = wceq 1654    e. wcel 1728   {cab 2429   {crab 2716    i^i cin 3308
This theorem is referenced by:  rabnc  3639  ixxin  10971  hashbclem  11739  phiprmpw  13203  submacs  14803  ablfacrp  15662  dfrhm2  15859  ordtbaslem  17290  ordtbas2  17293  ordtopn3  17298  ordtcld3  17301  ordthauslem  17485  pthaus  17708  xkohaus  17723  tsmsfbas  18195  minveclem3b  19367  shftmbl  19471  mumul  21002  ppiub  21026  lgsquadlem2  21177  cusgrasizeindslem2  21521  xppreima  24094  xpinpreima  24339  xpinpreima2  24340  measvuni  24603  subfacp1lem6  24906  cnambfre  26295  itg2addnclem2  26299  ftc1anclem6  26327  anrabdioph  26951  frisusgranb  28559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2721  df-v 2967  df-in 3316
  Copyright terms: Public domain W3C validator