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

Theorem elab2g 3175
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2g.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
elab2g.2  |-  B  =  { x  |  ph }
Assertion
Ref Expression
elab2g  |-  ( A  e.  V  ->  ( A  e.  B  <->  ps )
)
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    B( x)    V( x)

Proof of Theorem elab2g
StepHypRef Expression
1 elab2g.2 . . 3  |-  B  =  { x  |  ph }
21eleq2i 2541 . 2  |-  ( A  e.  B  <->  A  e.  { x  |  ph }
)
3 elab2g.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elabg 3174 . 2  |-  ( A  e.  V  ->  ( A  e.  { x  |  ph }  <->  ps )
)
52, 4syl5bb 265 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  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:  elab2  3176  elab4g  3177  eldif  3400  elun  3565  elin  3608  elprg  3975  elsncg  3983  eluni  4193  eliun  4274  eliin  4275  elopab  4709  elrn2g  5030  eldmg  5035  elrnmpt  5087  elrnmpt1  5089  elimag  5178  elong  5438  elrnmpt2g  6427  elrnmpt2res  6429  eloprabi  6874  tfrlem12  7125  elqsg  7433  elixp2  7544  isacn  8493  isfin1a  8740  isfin2  8742  isfin4  8745  isfin7  8749  isfin3ds  8777  elwina  9129  elina  9130  iswun  9147  eltskg  9193  elgrug  9235  elnp  9430  elnpi  9431  iscat  15656  isps  16526  isdir  16556  ismgm  16567  elsymgbas2  17100  mdetunilem9  19722  istopg  20002  isbasisg  20039  isptfin  20608  isufl  21006  isusp  21354  2sqlem9  24380  isplig  25988  isgrpo  26005  isass  26125  isexid  26126  ismgmOLD  26129  elghomlem2OLD  26171  elunop  27606  adjeu  27623  isarchi  28573  ispcmp  28758  eulerpartlemelr  29263  eulerpartlemgs2  29286  ballotlemfmpn  29400  ismfs  30259  dfon2lem3  30502  orderseqlem  30561  elno  30604  elaltxp  30813  heiborlem1  32207  heiborlem10  32216  nzss  36736  elrnmptf  37525  issal  38287  isuhgr  39304  isushgr  39305  isupgr  39330  isumgr  39340  isuspgr  39400  isusgr  39401  iscplgr  39646  isconngr  40103  isconngr1  40104  isuhgrALTV  40186  isushgrALTV  40187  ismgmALT  40367
  Copyright terms: Public domain W3C validator