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

Theorem elrab3 2937
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)
Hypothesis
Ref Expression
elrab.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elrab3  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem elrab3
StepHypRef Expression
1 elrab.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21elrab 2936 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 871 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   {crab 2560
This theorem is referenced by:  unimax  3877  fnse  6248  fin23lem30  7984  isf32lem5  7999  ublbneg  10318  negn0  10320  supminf  10321  isacs1i  13575  subgacs  14668  nsgacs  14669  odngen  14904  lssacs  15740  mretopd  16845  txkgen  17362  xkoco1cn  17367  xkoco2cn  17368  xkoinjcn  17397  ordthmeolem  17508  shft2rab  18883  sca2rab  18887  lhop1lem  19376  ftalem5  20330  vmasum  20471  cvmliftmolem1  23827  eupath2lem3  23918  nobndlem5  24421  nobndup  24425  nobnddown  24426  neibastop3  26414  fdc  26558  fnelfp  26858  fnelnfp  26860  diophren  26999  islmodfg  27270  sdrgacs  27612  stoweidlem34  27886  nbgranself  28283  pclvalN  30701  dvhb1dimN  31797  hdmaplkr  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803
  Copyright terms: Public domain W3C validator