MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elab2 Unicode version

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
StepHypRef Expression
1 elab2.1 . 2
2 elab2.2 . . 3
3 elab2.3 . . 3
42, 3elab2g 3218 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator