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

Theorem elrab3 2924
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 2923 . 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 1623    e. wcel 1684   {crab 2547
This theorem is referenced by:  unimax  3861  fnse  6232  fin23lem30  7968  isf32lem5  7983  ublbneg  10302  negn0  10304  supminf  10305  isacs1i  13559  subgacs  14652  nsgacs  14653  odngen  14888  lssacs  15724  mretopd  16829  txkgen  17346  xkoco1cn  17351  xkoco2cn  17352  xkoinjcn  17381  ordthmeolem  17492  shft2rab  18867  sca2rab  18871  lhop1lem  19360  ftalem5  20314  vmasum  20455  cvmliftmolem1  23812  eupath2lem3  23903  nobndlem5  24350  nobndup  24354  nobnddown  24355  neibastop3  26311  fdc  26455  fnelfp  26755  fnelnfp  26757  diophren  26896  islmodfg  27167  sdrgacs  27509  stoweidlem34  27783  nbgranself  28149  pclvalN  30079  dvhb1dimN  31175  hdmaplkr  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790
  Copyright terms: Public domain W3C validator