Theorem elab2 3087

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

Step	Hyp	Ref	Expression
1		elab2.1	. 2
2		elab2.2	. . 3
3		elab2.3	. . 3
4	2, 3	elab2g 3086	. 2
5	1, 4	ax-mp 5	1

Syntax hints:  ->wi 4  <->wb 178  =wceq 1687  e.wcel 1749  {cab 2408  cvv 2951

This theorem is referenced by:  elpw  3843  elint  4109  opabid  4568  elrn2  5050  elimasn  5166  oprabid  6085  tfrlem3a  6795  cardprclem  8096  iunfictbso  8231  aceq3lem  8237  dfac5lem4  8243  kmlem9  8274  domtriomlem  8558  ltexprlem3  9153  ltexprlem4  9154  reclem2pr  9163  reclem3pr  9164  supsrlem  9224  supmul1  10241  supmullem1  10242  supmullem2  10243  supmul  10244  sqrlem6  12678  infcvgaux2i  13260  mertenslem1  13284  mertenslem2  13285  4sqlem12  13957  conjnmzb  15718  sylow3lem2  16064  mdetunilem9  18128  txuni2  18842  xkoopn  18866  met2ndci  19797  2sqlem8  22452  2sqlem11  22455  eulerpartlemt  26457  eulerpartlemr  26460  eulerpartlemn  26467  subfacp1lem3  26773  subfacp1lem5  26775  soseq  27417  nofulllem5  27549  supaddc  28088  supadd  28089  heiborlem1  28381  heiborlem6  28386  heiborlem8  28388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403

This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-v 2953