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

Theorem elabg 2916
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)
Hypothesis
Ref Expression
elabg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elabg  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem elabg
StepHypRef Expression
1 nfcv 2420 . 2  |-  F/_ x A
2 nfv 1606 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 2913 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1624    e. wcel 1685   {cab 2270
This theorem is referenced by:  elab2g  2917  intmin3  3891  finds  4681  elxpi  4704  elfi  7162  inficl  7173  dffi3  7179  scott0  7551  elgch  8239  nqpr  8633  hashf1lem1  11387  efgcpbllemb  15058  frgpuplem  15075  lspsn  15753  eltg  16689  eltg2  16690  fbssfi  17526  mpfind  19422  pf1ind  19432  elabreximd  23032  ballotlemfmpn  23046  eloi  24484  elixp2b  24553  domrancur1b  24599  domrancur1c  24601  isoriso2  24612  isdir2  24691  intopcoaconlem3b  24937  iscol2  25492  islocfin  25695  setindtrs  26517  rngunsnply  26777  afvelrnb  27402  afvelrnb0  27403  islshpkrN  28577
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791
  Copyright terms: Public domain W3C validator