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

Theorem elab3 3113
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 3112 . 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 1369    e. wcel 1756   {cab 2429   _Vcvv 2972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974
This theorem is referenced by:  fvelrnb  5739  elrnmpt2  6203  ovelrn  6239  isfi  7333  isnum2  8115  pm54.43lem  8169  isfin3  8465  isfin5  8468  isfin6  8469  genpelv  9169  iswrd  12237  4sqlem2  14010  vdwapval  14034  ismnd  15417  isghm  15747  issrng  16935  lspsnel  17084  lspprel  17175  iscss  18108  ellspd  18230  ellspdOLD  18231  istps  18541  islp  18744  is2ndc  19050  elpt  19145  itg2l  21207  elply  21663  rngunsnply  29530  isline  33383  ispointN  33386  ispsubsp  33389  ispsubclN  33581  islaut  33727  ispautN  33743  istendo  34404
  Copyright terms: Public domain W3C validator