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

Theorem elabg 3251
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 2629 . 2  |-  F/_ x A
2 nfv 1683 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 3248 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   {cab 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115
This theorem is referenced by:  elab2g  3252  intmin3  4310  elxpi  5015  finds  6705  elfi  7872  inficl  7884  dffi3  7890  scott0  8303  elgch  8999  nqpr  9391  hashf1lem1  12469  cshword  12724  lubval  15470  glbval  15483  efgcpbllemb  16576  frgpuplem  16593  lspsn  17443  mpfind  17992  pf1ind  18178  eltg  19241  eltg2  19242  fbssfi  20089  elabreximd  27098  abfmpunirn  27178  orvcval  28052  wfrlem15  28950  islocfin  29784  setindtrs  30587  rngunsnply  30743  nzss  30838  elabrexg  31028  upbdrech  31098  afvelrnb  31731  afvelrnb0  31732  ismgmALT  31939  ismgmALT2  31993  islshpkrN  33926
  Copyright terms: Public domain W3C validator