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

Theorem elrab3 3258
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 3257 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 903 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395    e. wcel 1819   {crab 2811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111
This theorem is referenced by:  unimax  4287  fnelfp  6100  fnelnfp  6102  fnse  6916  fin23lem30  8739  isf32lem5  8754  ublbneg  11191  negn0  11193  supminf  11194  sadval  14118  smuval  14143  isacs1i  15074  isinito  15406  istermo  15407  subgacs  16363  nsgacs  16364  odngen  16724  lssacs  17740  mretopd  19720  txkgen  20279  xkoco1cn  20284  xkoco2cn  20285  xkoinjcn  20314  ordthmeolem  20428  shft2rab  22045  sca2rab  22049  lhop1lem  22540  ftalem5  23476  vmasum  23617  israg  24200  ebtwntg  24412  nbgranself  24561  eupath2lem3  25106  cvmliftmolem1  28923  nobndlem5  29673  nobndup  29677  nobnddown  29678  neibastop3  30385  fdc  30443  diophren  30951  islmodfg  31219  sdrgacs  31354  radcnvrat  31399  dvdslcm  31408  stoweidlem34  32019  pclvalN  35757  dvhb1dimN  36855  hdmaplkr  37786
  Copyright terms: Public domain W3C validator