Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eluni | Structured version Visualization version Unicode version |
Description: Membership in class union. (Contributed by NM, 22-May-1994.) |
Ref | Expression |
---|---|
eluni |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3212 | . 2 | |
2 | elex 3212 | . . . 4 | |
3 | 2 | adantr 481 | . . 3 |
4 | 3 | exlimiv 1858 | . 2 |
5 | eleq1 2689 | . . . . 5 | |
6 | 5 | anbi1d 741 | . . . 4 |
7 | 6 | exbidv 1850 | . . 3 |
8 | df-uni 4437 | . . 3 | |
9 | 7, 8 | elab2g 3353 | . 2 |
10 | 1, 4, 9 | pm5.21nii 368 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wceq 1483 wex 1704 wcel 1990 cvv 3200 cuni 4436 |
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 df-uni 4437 |
This theorem is referenced by: eluni2 4440 elunii 4441 eluniab 4447 uniun 4456 uniin 4457 uniss 4458 unissb 4469 dftr2 4754 unipw 4918 dmuni 5334 fununi 5964 elunirn 6509 uniex2 6952 uniuni 6971 mpt2xopxnop0 7341 wfrfun 7425 wfrlem17 7431 tfrlem7 7479 tfrlem9a 7482 inf2 8520 inf3lem2 8526 rankwflemb 8656 cardprclem 8805 carduni 8807 iunfictbso 8937 kmlem3 8974 kmlem4 8975 cfub 9071 isf34lem4 9199 grothtsk 9657 suplem1pr 9874 toprntopon 20729 isbasis2g 20752 tgval2 20760 ntreq0 20881 cmpsublem 21202 cmpsub 21203 cmpcld 21205 is1stc2 21245 alexsubALTlem3 21853 alexsubALT 21855 frrlem5c 31786 fnessref 32352 bj-restuni 33050 truniALT 38751 truniALTVD 39114 unisnALT 39162 elunif 39175 ssfiunibd 39523 stoweidlem27 40244 stoweidlem48 40265 setrec1lem3 42436 setrec1 42438 |
Copyright terms: Public domain | W3C validator |