Theorem elab2g 3248

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2g.1
elab2g.2

Assertion

Ref	Expression
elab2g

Distinct variable groups:   ,   ,

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.2	. . 3
2	1	eleq2i 2535	. 2
3		elab2g.1	. . 3
4	3	elabg 3247	. 2
5	2, 4	syl5bb 257	1

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

This theorem is referenced by:  elab2  3249  elab4g  3250  eldif  3485  elun  3644  elin  3686  elprg  4045  elsncg  4052  eluni  4252  eliun  4335  eliin  4336  elopab  4760  elong  4891  elrn2g  5198  eldmg  5203  elrnmpt  5254  elrnmpt1  5256  elimag  5346  elrnmpt2g  6414  elrnmpt2res  6416  eloprabi  6862  tfrlem12  7077  elqsg  7382  elixp2  7493  isacn  8446  isfin1a  8693  isfin2  8695  isfin4  8698  isfin7  8702  isfin3ds  8730  elwina  9085  elina  9086  iswun  9103  eltskg  9149  elgrug  9191  elnp  9386  elnpi  9387  iscat  15069  isps  15832  isdir  15862  ismgm  15873  elsymgbas2  16406  mdetunilem9  19122  istopg  19404  isbasisg  19448  isptfin  20017  isufl  20414  isusp  20764  2sqlem9  23648  isplig  25179  isgrpo  25198  isass  25318  isexid  25319  ismgmOLD  25322  elghomlem2OLD  25364  elunop  26791  adjeu  26808  isarchi  27726  ispcmp  27860  eulerpartlemelr  28296  eulerpartlemgs2  28319  ballotlemfmpn  28433  ismfs  28909  dfon2lem3  29217  orderseqlem  29332  elno  29406  elaltxp  29625  heiborlem1  30307  heiborlem10  30316  nzss  31222  isuhgr  32366  isushgr  32367  ismgmALT  32547

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