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

Theorem elab3 3253
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 3252 . 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 1395    e. wcel 1819   {cab 2442   _Vcvv 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111
This theorem is referenced by:  fvelrnb  5920  elrnmpt2  6414  ovelrn  6450  isfi  7558  isnum2  8343  pm54.43lem  8397  isfin3  8693  isfin5  8696  isfin6  8697  genpelv  9395  iswrd  12554  iswrdOLD  12555  4sqlem2  14479  vdwapval  14503  ismndOLD  16053  isghm  16394  issrng  17626  lspsnel  17776  lspprel  17867  iscss  18841  ellspd  18963  ellspdOLD  18964  istps  19564  islp  19768  is2ndc  20073  elpt  20199  itg2l  22262  elply  22718  isismt  24047  rngunsnply  31305  isline  35585  ispointN  35588  ispsubsp  35591  ispsubclN  35783  islaut  35929  ispautN  35945  istendo  36608
  Copyright terms: Public domain W3C validator