Theorem elabg 3247

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:   ,   ,

Proof of Theorem elabg

Step	Hyp	Ref	Expression
1		nfcv 2619	. 2
2		nfv 1707	. 2
3		elabg.1	. 2
4	1, 2, 3	elabgf 3244	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442

This theorem is referenced by:  elab2g  3248  intmin3  4315  elxpi  5020  finds  6726  elfi  7893  inficl  7905  dffi3  7911  scott0  8325  elgch  9021  nqpr  9413  hashf1lem1  12504  cshword  12762  lubval  15614  glbval  15627  efgcpbllemb  16773  frgpuplem  16790  lspsn  17648  mpfind  18205  pf1ind  18391  eltg  19458  eltg2  19459  islocfin  20018  fbssfi  20338  elabreximd  27408  abfmpunirn  27490  orvcval  28396  wfrlem15  29357  setindtrs  30967  rngunsnply  31122  nzss  31222  elabrexg  31430  afvelrnb  32248  afvelrnb0  32249  dfiso2  32568  islshpkrN  34845

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