Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elab2g | Unicode version |
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elab2g.1 | |
elab2g.2 |
Ref | Expression |
---|---|
elab2g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab2g.2 | . . 3 | |
2 | 1 | eleq2i 2145 | . 2 |
3 | elab2g.1 | . . 3 | |
4 | 3 | elabg 2739 | . 2 |
5 | 2, 4 | syl5bb 190 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 wceq 1284 wcel 1433 cab 2067 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-tru 1287 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-v 2603 |
This theorem is referenced by: elab2 2741 elab4g 2742 eldif 2982 elun 3113 elin 3155 elsng 3413 elprg 3418 eluni 3604 eliun 3682 eliin 3683 elopab 4013 elong 4128 opeliunxp 4413 elrn2g 4543 eldmg 4548 elrnmpt 4601 elrnmpt1 4603 elimag 4692 elrnmpt2g 5633 eloprabi 5842 tfrlem3ag 5947 elqsg 6179 1idprl 6780 1idpru 6781 recexprlemell 6812 recexprlemelu 6813 |
Copyright terms: Public domain | W3C validator |