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

Theorem inrab 3558
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 2660 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2660 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2ineq12i 3485 . 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 2660 . . 3  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  { x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
5 inab 3554 . . . 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 2501 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  /\ 
ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2412 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
94, 8eqtr4i 2412 . 2  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2412 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 1649    e. wcel 1717   {cab 2375   {crab 2655    i^i cin 3264
This theorem is referenced by:  rabnc  3596  ixxin  10867  hashbclem  11630  phiprmpw  13094  submacs  14694  ablfacrp  15553  dfrhm2  15750  ordtbaslem  17176  ordtbas2  17179  ordtopn3  17184  ordtcld3  17187  ordthauslem  17371  pthaus  17593  xkohaus  17608  tsmsfbas  18080  minveclem3b  19198  shftmbl  19302  mumul  20833  ppiub  20857  lgsquadlem2  21008  cusgrasizeindslem2  21351  xppreima  23903  xpinpreima  24110  xpinpreima2  24111  measvuni  24364  subfacp1lem6  24652  itg2addnclem2  25960  anrabdioph  26532  frisusgranb  27752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-v 2903  df-in 3272
  Copyright terms: Public domain W3C validator