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

Theorem elrab3 3102
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 3101 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 873 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1654    e. wcel 1728   {crab 2716
This theorem is referenced by:  unimax  4078  fnse  6499  fin23lem30  8260  isf32lem5  8275  ublbneg  10598  negn0  10600  supminf  10601  sadval  13006  smuval  13031  isacs1i  13920  subgacs  15013  nsgacs  15014  odngen  15249  lssacs  16081  mretopd  17194  txkgen  17722  xkoco1cn  17727  xkoco2cn  17728  xkoinjcn  17757  ordthmeolem  17871  shft2rab  19442  sca2rab  19446  lhop1lem  19935  ftalem5  20897  vmasum  21038  nbgranself  21484  eupath2lem3  21739  cvmliftmolem1  25003  nobndlem5  25686  nobndup  25690  nobnddown  25691  neibastop3  26433  fdc  26491  fnelfp  26848  fnelnfp  26850  diophren  26986  islmodfg  27256  sdrgacs  27598  stoweidlem34  27871  pclvalN  30861  dvhb1dimN  31957  hdmaplkr  32888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2721  df-v 2967
  Copyright terms: Public domain W3C validator