Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > risset | Structured version Visualization version Unicode version |
Description: Two ways to say " belongs to ." (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
risset |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exancom 1787 | . 2 | |
2 | df-rex 2918 | . 2 | |
3 | df-clel 2618 | . 2 | |
4 | 1, 2, 3 | 3bitr4ri 293 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wceq 1483 wex 1704 wcel 1990 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-clel 2618 df-rex 2918 |
This theorem is referenced by: reueq 3404 reuind 3411 0el 3939 iunid 4575 reusv3 4876 sucel 5798 fvmptt 6300 releldm2 7218 qsid 7813 zorng 9326 rereccl 10743 nndiv 11061 zq 11794 4fvwrd4 12459 wrdlen1 13343 incexc2 14570 ruclem12 14970 phisum 15495 conjnmzb 17695 symgmov1 17812 pgpfac1lem2 18474 pgpfac1lem4 18477 mat1dimelbas 20277 mat1dimbas 20278 chmaidscmat 20653 unisngl 21330 fmid 21764 dcubic 24573 fusgrn0degnn0 26395 chscllem2 28497 disjunsn 29407 ballotlemsima 30577 dfon2lem8 31695 brimg 32044 dfrecs2 32057 altopelaltxp 32083 prtlem9 34149 prtlem11 34151 prter2 34166 2llnmat 34810 2lnat 35070 cdlemefrs29bpre1 35685 elnn0rabdioph 37367 fiphp3d 37383 |
Copyright terms: Public domain | W3C validator |