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

Theorem elab2 3028
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2.1  |-  A  e. 
_V
elab2.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
elab2.3  |-  B  =  { x  |  ph }
Assertion
Ref Expression
elab2  |-  ( A  e.  B  <->  ps )
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    B( x)

Proof of Theorem elab2
StepHypRef Expression
1 elab2.1 . 2  |-  A  e. 
_V
2 elab2.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
3 elab2.3 . . 3  |-  B  =  { x  |  ph }
42, 3elab2g 3027 . 2  |-  ( A  e.  _V  ->  ( A  e.  B  <->  ps )
)
51, 4ax-mp 8 1  |-  ( A  e.  B  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   {cab 2373   _Vcvv 2899
This theorem is referenced by:  elpw  3748  elint  3998  opabid  4402  elrn2  5049  elimasn  5169  oprabid  6044  cardprclem  7799  iunfictbso  7928  aceq3lem  7934  dfac5lem4  7940  kmlem9  7971  domtriomlem  8255  ltexprlem3  8848  ltexprlem4  8849  reclem2pr  8858  reclem3pr  8859  supsrlem  8919  supmul1  9905  supmullem1  9906  supmullem2  9907  supmul  9908  sqrlem6  11980  infcvgaux2i  12564  mertenslem1  12588  mertenslem2  12589  4sqlem12  13251  conjnmzb  14967  sylow3lem2  15189  txuni2  17518  xkoopn  17542  met2ndci  18442  2sqlem8  21023  2sqlem11  21026  subfacp1lem3  24647  subfacp1lem5  24649  soseq  25278  nofulllem5  25384  supaddc  25947  supadd  25948  heiborlem1  26211  heiborlem6  26216  heiborlem8  26218
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901
  Copyright terms: Public domain W3C validator