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 2231 | . 2 |
3 | elab2g.1 | . . 3 | |
4 | 3 | elabg 2867 | . 2 |
5 | 2, 4 | syl5bb 191 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1342 wcel 2135 cab 2150 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 |
This theorem is referenced by: elab2 2869 elab4g 2870 eldif 3120 elun 3258 elin 3300 elsng 3585 elprg 3590 eluni 3786 eliun 3864 eliin 3865 elopab 4230 elong 4345 opeliunxp 4653 elrn2g 4788 eldmg 4793 elrnmpt 4847 elrnmpt1 4849 elimag 4944 elrnmpog 5945 eloprabi 6156 tfrlem3ag 6268 tfr1onlem3ag 6296 tfrcllemsucaccv 6313 elqsg 6542 elixp2 6659 isomni 7091 ismkv 7108 iswomni 7120 1idprl 7522 1idpru 7523 recexprlemell 7554 recexprlemelu 7555 mertenslemub 11461 mertenslemi1 11462 mertenslem2 11463 istopg 12538 isbasisg 12583 |
Copyright terms: Public domain | W3C validator |