Theorem elab2 3219

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 3218	. 2
5	1, 4	ax-mp 5	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1370  e.wcel 1758  {cab 2439  cvv 3081

This theorem is referenced by:  elpw  3982  elint  4251  opabid  4713  elrn2  5196  elimasn  5313  oprabid  6246  tfrlem3a  6970  cardprclem  8286  iunfictbso  8421  aceq3lem  8427  dfac5lem4  8433  kmlem9  8464  domtriomlem  8748  ltexprlem3  9344  ltexprlem4  9345  reclem2pr  9354  reclem3pr  9355  supsrlem  9415  supmul1  10432  supmullem1  10433  supmullem2  10434  supmul  10435  sqrlem6  12895  infcvgaux2i  13478  mertenslem1  13502  mertenslem2  13503  4sqlem12  14175  conjnmzb  15940  sylow3lem2  16288  mdetunilem9  18694  txuni2  19537  xkoopn  19561  met2ndci  20496  2sqlem8  23111  2sqlem11  23114  eulerpartlemt  27210  eulerpartlemr  27213  eulerpartlemn  27220  subfacp1lem3  27526  subfacp1lem5  27528  soseq  28171  nofulllem5  28303  supaddc  28877  supadd  28878  heiborlem1  29170  heiborlem6  29175  heiborlem8  29177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083