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

Theorem elrab3 3262
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 3261 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 901 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115
This theorem is referenced by:  unimax  4281  fnelfp  6087  fnelnfp  6089  fnse  6897  fin23lem30  8718  isf32lem5  8733  ublbneg  11162  negn0  11164  supminf  11165  sadval  13958  smuval  13983  isacs1i  14905  subgacs  16028  nsgacs  16029  odngen  16390  lssacs  17393  mretopd  19356  txkgen  19885  xkoco1cn  19890  xkoco2cn  19891  xkoinjcn  19920  ordthmeolem  20034  shft2rab  21651  sca2rab  21655  lhop1lem  22146  ftalem5  23075  vmasum  23216  israg  23779  nbgranself  24107  eupath2lem3  24652  cvmliftmolem1  28363  nobndlem5  29030  nobndup  29034  nobnddown  29035  neibastop3  29781  fdc  29839  diophren  30349  islmodfg  30619  sdrgacs  30755  dvdslcm  30804  stoweidlem34  31334  pclvalN  34686  dvhb1dimN  35782  hdmaplkr  36713
  Copyright terms: Public domain W3C validator