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

Theorem elrab3 3107
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 3106 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 889 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362    e. wcel 1755   {crab 2709
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
This theorem is referenced by:  unimax  4115  fnelfp  5893  fnelnfp  5895  fnse  6678  fin23lem30  8499  isf32lem5  8514  ublbneg  10926  negn0  10928  supminf  10929  sadval  13634  smuval  13659  isacs1i  14577  subgacs  15695  nsgacs  15696  odngen  16055  lssacs  16969  mretopd  18537  txkgen  19066  xkoco1cn  19071  xkoco2cn  19072  xkoinjcn  19101  ordthmeolem  19215  shft2rab  20832  sca2rab  20836  lhop1lem  21326  ftalem5  22298  vmasum  22439  nbgranself  23167  eupath2lem3  23422  cvmliftmolem1  27017  nobndlem5  27683  nobndup  27687  nobnddown  27688  neibastop3  28424  fdc  28482  diophren  28994  islmodfg  29264  sdrgacs  29400  stoweidlem34  29672  pclvalN  33104  dvhb1dimN  34200  hdmaplkr  35131
  Copyright terms: Public domain W3C validator