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

Theorem elab3 3262
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 3261 . 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 184    = wceq 1379    e. wcel 1767   {cab 2452   _Vcvv 3118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120
This theorem is referenced by:  fvelrnb  5921  elrnmpt2  6410  ovelrn  6446  isfi  7551  isnum2  8338  pm54.43lem  8392  isfin3  8688  isfin5  8691  isfin6  8692  genpelv  9390  iswrd  12530  4sqlem2  14342  vdwapval  14366  ismndOLD  15798  isghm  16138  issrng  17368  lspsnel  17518  lspprel  17609  iscss  18581  ellspd  18703  ellspdOLD  18704  istps  19304  islp  19507  is2ndc  19813  elpt  19939  itg2l  22002  elply  22458  isismt  23785  rngunsnply  31057  isline  34941  ispointN  34944  ispsubsp  34947  ispsubclN  35139  islaut  35285  ispautN  35301  istendo  35962
  Copyright terms: Public domain W3C validator