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

Theorem elrab3 3219
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 3218 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
32baib 896 1  |-  ( A  e.  B  ->  ( A  e.  { x  e.  B  |  ph }  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370    e. wcel 1758   {crab 2800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rab 2805  df-v 3074
This theorem is referenced by:  unimax  4230  fnelfp  6010  fnelnfp  6012  fnse  6794  fin23lem30  8617  isf32lem5  8632  ublbneg  11045  negn0  11047  supminf  11048  sadval  13765  smuval  13790  isacs1i  14709  subgacs  15830  nsgacs  15831  odngen  16192  lssacs  17166  mretopd  18823  txkgen  19352  xkoco1cn  19357  xkoco2cn  19358  xkoinjcn  19387  ordthmeolem  19501  shft2rab  21118  sca2rab  21122  lhop1lem  21613  ftalem5  22542  vmasum  22683  israg  23229  nbgranself  23492  eupath2lem3  23747  cvmliftmolem1  27309  nobndlem5  27976  nobndup  27980  nobnddown  27981  neibastop3  28726  fdc  28784  diophren  29295  islmodfg  29565  sdrgacs  29701  stoweidlem34  29972  pclvalN  33853  dvhb1dimN  34949  hdmaplkr  35880
  Copyright terms: Public domain W3C validator