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

Theorem elrab3 3199
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 3198 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 915 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1446    e. wcel 1889   {crab 2743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049
This theorem is referenced by:  unimax  4236  fnelfp  6097  fnelnfp  6099  fnse  6918  fin23lem30  8777  isf32lem5  8792  negn0  10055  ublbneg  11255  supminf  11257  supminfOLD  11258  sadval  14442  smuval  14467  dvdslcm  14575  lcmsOLD  14596  dvdslcmf  14616  isacs1i  15575  isinito  15907  istermo  15908  subgacs  16864  nsgacs  16865  odngen  17238  lssacs  18202  mretopd  20120  txkgen  20679  xkoco1cn  20684  xkoco2cn  20685  xkoinjcn  20714  ordthmeolem  20828  shft2rab  22473  sca2rab  22477  lhop1lem  22977  ftalem5  24013  ftalem5OLD  24015  vmasum  24156  israg  24754  ebtwntg  25024  nbgranself  25174  eupath2lem3  25719  cvmliftmolem1  30016  nobndlem5  30597  nobndup  30601  nobnddown  30602  neibastop3  31030  fdc  32086  pclvalN  33467  dvhb1dimN  34565  hdmaplkr  35496  diophren  35668  islmodfg  35939  sdrgacs  36079  radcnvrat  36674  stoweidlem34  37905
  Copyright terms: Public domain W3C validator