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

Theorem elabg 3083
 Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)
Hypothesis
Ref Expression
elabg.1
Assertion
Ref Expression
elabg
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem elabg
StepHypRef Expression
1 nfcv 2572 . 2
2 nfv 1629 . 2
3 elabg.1 . 2
41, 2, 3elabgf 3080 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wceq 1652   wcel 1725  cab 2422 This theorem is referenced by:  elab2g  3084  intmin3  4078  finds  4871  elxpi  4894  elfi  7418  inficl  7430  dffi3  7436  scott0  7810  elgch  8497  nqpr  8891  hashf1lem1  11704  efgcpbllemb  15387  frgpuplem  15404  lspsn  16078  eltg  17022  eltg2  17023  fbssfi  17869  mpfind  19965  pf1ind  19975  elabreximd  23991  abfmpunirn  24064  orvcval  24715  wfrlem15  25552  islocfin  26376  setindtrs  27096  rngunsnply  27355  afvelrnb  28003  afvelrnb0  28004  cshword  28235  islshpkrN  29918 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958
 Copyright terms: Public domain W3C validator