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

Theorem elab3 3167
Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)
Hypotheses
Ref Expression
elab3.1  |-  ( ps 
->  A  e.  _V )
elab3.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elab3  |-  ( A  e.  { x  | 
ph }  <->  ps )
Distinct variable groups:    ps, x    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem elab3
StepHypRef Expression
1 elab3.1 . 2  |-  ( ps 
->  A  e.  _V )
2 elab3.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32elab3g 3166 . 2  |-  ( ( ps  ->  A  e.  _V )  ->  ( A  e.  { x  | 
ph }  <->  ps )
)
41, 3ax-mp 5 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1872   {cab 2414   _Vcvv 3022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024
This theorem is referenced by:  fvelrnb  5872  elrnmpt2  6367  ovelrn  6403  isfi  7547  isnum2  8331  pm54.43lem  8385  isfin3  8677  isfin5  8680  isfin6  8681  genpelv  9376  iswrd  12620  iswrdOLD  12621  4sqlem2  14836  vdwapval  14866  ismndOLD  16485  isghm  16826  issrng  18021  lspsnel  18169  lspprel  18260  iscss  19188  ellspd  19302  istps  19893  islp  20098  is2ndc  20403  elpt  20529  itg2l  22629  elply  23091  isismt  24521  isline  33216  ispointN  33219  ispsubsp  33222  ispsubclN  33414  islaut  33560  ispautN  33576  istendo  34239  rngunsnply  35952
  Copyright terms: Public domain W3C validator