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

Theorem elab3 3081
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 3080 . 2  |-  ( ( ps  ->  A  e.  _V )  ->  ( A  e.  { x  | 
ph }  <->  ps )
)
41, 3ax-mp 8 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {cab 2421   _Vcvv 2948
This theorem is referenced by:  fvelrnb  5766  elrnmpt2  6175  ovelrn  6214  isfi  7123  isnum2  7824  pm54.43lem  7878  isfin3  8168  isfin5  8171  isfin6  8172  genpelv  8869  iswrd  11721  4sqlem2  13309  vdwapval  13333  ismnd  14684  isghm  14998  issrng  15930  lspsnel  16071  lspprel  16158  iscss  16902  istps  16993  islp  17196  is2ndc  17501  elpt  17596  itg2l  19613  elply  20106  ellspd  27222  rngunsnply  27346  isline  30473  ispointN  30476  ispsubsp  30479  ispsubclN  30671  islaut  30817  ispautN  30833  istendo  31494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950
  Copyright terms: Public domain W3C validator