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

Theorem inrab 3610
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 3538 . 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 3606 . . . 4  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
6 anandi 817 . . . . 5  |-  ( ( x  e.  A  /\  ( ph  /\  ps )
)  <->  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps )
) )
76abbii 2545 . . . 4  |-  { x  |  ( x  e.  A  /\  ( ph  /\ 
ps ) ) }  =  { x  |  ( ( x  e.  A  /\  ph )  /\  ( x  e.  A  /\  ps ) ) }
85, 7eqtr4i 2456 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )  =  {
x  |  ( x  e.  A  /\  ( ph  /\  ps ) ) }
94, 8eqtr4i 2456 . 2  |-  { x  e.  A  |  ( ph  /\  ps ) }  =  ( { x  |  ( x  e.  A  /\  ph ) }  i^i  { x  |  ( x  e.  A  /\  ps ) } )
103, 9eqtr4i 2456 1  |-  ( { x  e.  A  |  ph }  i^i  { x  e.  A  |  ps } )  =  {
x  e.  A  | 
( ph  /\  ps ) }
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1362    e. wcel 1755   {cab 2419   {crab 2709    i^i cin 3315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-in 3323
This theorem is referenced by:  rabnc  3649  ixxin  11304  hashbclem  12188  phiprmpw  13833  submacs  15474  ablfacrp  16540  dfrhm2  16741  ordtbaslem  18633  ordtbas2  18636  ordtopn3  18641  ordtcld3  18644  ordthauslem  18828  pthaus  19052  xkohaus  19067  tsmsfbas  19539  minveclem3b  20756  shftmbl  20861  mumul  22403  ppiub  22427  lgsquadlem2  22578  cusgrasizeindslem2  23204  xppreima  25787  xpinpreima  26189  xpinpreima2  26190  measvuni  26481  subfacp1lem6  26920  cnambfre  28281  itg2addnclem2  28285  ftc1anclem6  28313  anrabdioph  28961  frisusgranb  30432  numclwwlkdisj  30516  numclwwlk3lem  30544
  Copyright terms: Public domain W3C validator