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

Theorem elabg 3233
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 2605 . 2  |-  F/_ x A
2 nfv 1694 . 2  |-  F/ x ps
3 elabg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabgf 3230 1  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804   {cab 2428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097
This theorem is referenced by:  elab2g  3234  intmin3  4300  elxpi  5005  finds  6711  elfi  7875  inficl  7887  dffi3  7893  scott0  8307  elgch  9003  nqpr  9395  hashf1lem1  12486  cshword  12744  lubval  15593  glbval  15606  efgcpbllemb  16752  frgpuplem  16769  lspsn  17627  mpfind  18184  pf1ind  18370  eltg  19436  eltg2  19437  islocfin  19996  fbssfi  20316  elabreximd  27386  abfmpunirn  27468  orvcval  28374  wfrlem15  29333  setindtrs  30943  rngunsnply  31098  nzss  31198  elabrexg  31384  afvelrnb  32202  afvelrnb0  32203  islshpkrN  34720
  Copyright terms: Public domain W3C validator