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

Theorem elrab3 3095
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 3094 . 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 1653    e. wcel 1726   {crab 2711
This theorem is referenced by:  unimax  4051  fnse  6465  fin23lem30  8224  isf32lem5  8239  ublbneg  10562  negn0  10564  supminf  10565  sadval  12970  smuval  12995  isacs1i  13884  subgacs  14977  nsgacs  14978  odngen  15213  lssacs  16045  mretopd  17158  txkgen  17686  xkoco1cn  17691  xkoco2cn  17692  xkoinjcn  17721  ordthmeolem  17835  shft2rab  19406  sca2rab  19410  lhop1lem  19899  ftalem5  20861  vmasum  21002  nbgranself  21448  eupath2lem3  21703  cvmliftmolem1  24970  nobndlem5  25653  nobndup  25657  nobnddown  25658  neibastop3  26393  fdc  26451  fnelfp  26738  fnelnfp  26740  diophren  26876  islmodfg  27146  sdrgacs  27488  stoweidlem34  27761  pclvalN  30749  dvhb1dimN  31845  hdmaplkr  32776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
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 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960
  Copyright terms: Public domain W3C validator