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

Theorem elabg 3174
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 2612 . 2  |-  F/_ x A
2 nfv 1769 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 3171 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452    e. wcel 1904   {cab 2457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033
This theorem is referenced by:  elab2g  3175  intmin3  4254  elxpi  4855  finds  6738  wfrlem15  7068  elfi  7945  inficl  7957  dffi3  7963  scott0  8375  elgch  9065  nqpr  9457  hashf1lem1  12659  cshword  12947  trclublem  13134  cotrtrclfv  13153  dfiso2  15755  lubval  16308  glbval  16321  efgcpbllemb  17483  frgpuplem  17500  lspsn  18303  mpfind  18836  pf1ind  19020  eltg  20049  eltg2  20050  islocfin  20609  fbssfi  20930  elabreximd  28223  abfmpunirn  28327  orvcval  29363  poimirlem3  32007  poimirlem25  32029  islshpkrN  32757  setindtrs  35951  rngunsnply  36110  frege55lem1c  36583  nzss  36736  elabrexg  37432  ismea  38405  isome  38434  afvelrnb  38810  afvelrnb0  38811  cshword2  39125  isewlk  39808
  Copyright terms: Public domain W3C validator