Theorem elab2 3249

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

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

This theorem is referenced by:  elpw  4018  elint  4292  opabid  4759  elrn2  5247  elimasn  5367  oprabid  6323  tfrlem3a  7065  cardprclem  8381  iunfictbso  8516  aceq3lem  8522  dfac5lem4  8528  kmlem9  8559  domtriomlem  8843  ltexprlem3  9437  ltexprlem4  9438  reclem2pr  9447  reclem3pr  9448  supsrlem  9509  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  sqrlem6  13081  infcvgaux2i  13669  mertenslem1  13693  mertenslem2  13694  4sqlem12  14474  conjnmzb  16301  sylow3lem2  16648  mdetunilem9  19122  txuni2  20066  xkoopn  20090  met2ndci  21025  2sqlem8  23647  2sqlem11  23650  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemn  28320  subfacp1lem3  28626  subfacp1lem5  28628  soseq  29334  nofulllem5  29466  supaddc  30041  supadd  30042  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  cllem0  37751

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