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

Theorem elab3 3253
Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)
Hypotheses
Ref Expression
elab3.1
elab3.2
Assertion
Ref Expression
elab3
Distinct variable groups:   ,   ,

Proof of Theorem elab3
StepHypRef Expression
1 elab3.1 . 2
2 elab3.2 . . 3
32elab3g 3252 . 2
41, 3ax-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:  fvelrnb  5920  elrnmpt2  6415  ovelrn  6451  isfi  7559  isnum2  8347  pm54.43lem  8401  isfin3  8697  isfin5  8700  isfin6  8701  genpelv  9399  iswrd  12550  4sqlem2  14467  vdwapval  14491  ismndOLD  15926  isghm  16267  issrng  17499  lspsnel  17649  lspprel  17740  iscss  18714  ellspd  18836  ellspdOLD  18837  istps  19437  islp  19641  is2ndc  19947  elpt  20073  itg2l  22136  elply  22592  isismt  23921  rngunsnply  31122  isline  35463  ispointN  35466  ispsubsp  35469  ispsubclN  35661  islaut  35807  ispautN  35823  istendo  36486
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