MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrab3 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
Assertion
Ref Expression
elrab3
Distinct variable groups:   ,   ,   ,

Proof of Theorem elrab3
StepHypRef Expression
1 elrab.1 . . 3
21elrab 3257 . 2
32baib 903 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {crab 2811
This theorem is referenced by:  unimax  4285  fnelfp  6099  fnelnfp  6101  fnse  6917  fin23lem30  8743  isf32lem5  8758  ublbneg  11195  negn0  11197  supminf  11198  sadval  14106  smuval  14131  isacs1i  15054  subgacs  16236  nsgacs  16237  odngen  16597  lssacs  17613  mretopd  19593  txkgen  20153  xkoco1cn  20158  xkoco2cn  20159  xkoinjcn  20188  ordthmeolem  20302  shft2rab  21919  sca2rab  21923  lhop1lem  22414  ftalem5  23350  vmasum  23491  israg  24074  ebtwntg  24285  nbgranself  24434  eupath2lem3  24979  cvmliftmolem1  28726  nobndlem5  29456  nobndup  29460  nobnddown  29461  neibastop3  30180  fdc  30238  diophren  30747  islmodfg  31015  sdrgacs  31150  radcnvrat  31195  dvdslcm  31204  stoweidlem34  31816  isinito  32606  istermo  32607  pclvalN  35614  dvhb1dimN  36712  hdmaplkr  37643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111
  Copyright terms: Public domain W3C validator