ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elab2g Structured version   Unicode version

Theorem elab2g 2657
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2g.1
elab2g.2  {  |  }
Assertion
Ref Expression
elab2g  V
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()    V()

Proof of Theorem elab2g
StepHypRef Expression
1 elab2g.2 . . 3  {  |  }
21eleq2i 2077 . 2  {  |  }
3 elab2g.1 . . 3
43elabg 2656 . 2  V  {  |  }
52, 4syl5bb 181 1  V
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98   wceq 1223   wcel 1366   {cab 1999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-v 2528
This theorem is referenced by:  elab2  2658  elab4g  2659  eldif  2895  elun  3052  elin  3094  elprg  3356  elsncg  3361  eluni  3546  eliun  3624  eliin  3625  elopab  3958  elong  4048  opeliunxp  4310  elrn2g  4440  eldmg  4445  elrnmpt  4498  elrnmpt1  4500  elimag  4587  elrnmpt2g  5524  eloprabi  5733  tfrlem3ag  5834  elqsg  6055  1idprl  6415  1idpru  6416  recexprlemell  6443  recexprlemelu  6444
  Copyright terms: Public domain W3C validator