Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elab2g | Structured version Visualization version 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 2693 | . 2 |
3 | elab2g.1 | . . 3 | |
4 | 3 | elabg 3351 | . 2 |
5 | 2, 4 | syl5bb 272 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wcel 1990 cab 2608 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 |
This theorem is referenced by: elab2 3354 elab4g 3355 eldif 3584 elun 3753 elin 3796 elsng 4191 elprg 4196 eluni 4439 elintg 4483 eliun 4524 eliin 4525 elopab 4983 elrn2g 5313 eldmg 5319 elrnmpt 5372 elrnmpt1 5374 elimag 5470 elong 5731 elrnmpt2g 6772 elrnmpt2res 6774 eloprabi 7232 tfrlem12 7485 elqsg 7798 elixp2 7912 isacn 8867 isfin1a 9114 isfin2 9116 isfin4 9119 isfin7 9123 isfin3ds 9151 elwina 9508 elina 9509 iswun 9526 eltskg 9572 elgrug 9614 elnp 9809 elnpi 9810 iscat 16333 isps 17202 isdir 17232 ismgm 17243 elsymgbas2 17801 mdetunilem9 20426 istopg 20700 isbasisg 20751 isptfin 21319 isufl 21717 isusp 22065 2sqlem9 25152 isuhgr 25955 isushgr 25956 isupgr 25979 isumgr 25990 isuspgr 26047 isusgr 26048 iscplgr 26310 isconngr 27049 isconngr1 27050 isfrgr 27122 isplig 27328 isgrpo 27351 elunop 28731 adjeu 28748 isarchi 29736 ispcmp 29924 eulerpartlemelr 30419 eulerpartlemgs2 30442 ballotlemfmpn 30556 ismfs 31446 dfon2lem3 31690 orderseqlem 31749 elno 31799 elaltxp 32082 bj-ismoore 33059 heiborlem1 33610 heiborlem10 33619 isass 33645 isexid 33646 ismgmOLD 33649 elghomlem2OLD 33685 gneispace2 38430 nzss 38516 elrnmptf 39367 issal 40534 isome 40708 ismgmALT 41859 setrec1lem1 42434 |
Copyright terms: Public domain | W3C validator |