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

Theorem elab2 3249
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2.1
elab2.2
elab2.3
Assertion
Ref Expression
elab2
Distinct variable groups:   ,   ,

Proof of Theorem elab2
StepHypRef Expression
1 elab2.1 . 2
2 elab2.2 . . 3
3 elab2.3 . . 3
42, 3elab2g 3248 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442   cvv 3109
This theorem is referenced by:  elpw  4018  elint  4292  opabid  4759  elrn2  5247  elimasn  5367  oprabid  6323  tfrlem3a  7065  cardprclem  8381  iunfictbso  8516  aceq3lem  8522  dfac5lem4  8528  kmlem9  8559  domtriomlem  8843  ltexprlem3  9437  ltexprlem4  9438  reclem2pr  9447  reclem3pr  9448  supsrlem  9509  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  sqrlem6  13081  infcvgaux2i  13669  mertenslem1  13693  mertenslem2  13694  4sqlem12  14474  conjnmzb  16301  sylow3lem2  16648  mdetunilem9  19122  txuni2  20066  xkoopn  20090  met2ndci  21025  2sqlem8  23647  2sqlem11  23650  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemn  28320  subfacp1lem3  28626  subfacp1lem5  28628  soseq  29334  nofulllem5  29466  supaddc  30041  supadd  30042  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  cllem0  37751
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-v 3111
  Copyright terms: Public domain W3C validator