![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elunii | Structured version Visualization version Unicode version |
Description: Membership in class union. (Contributed by NM, 24-Mar-1995.) |
Ref | Expression |
---|---|
elunii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2529 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eleq1 2528 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anbi12d 722 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | spcegv 3147 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | anabsi7 833 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eluni 4215 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | sylibr 217 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-uni 4213 |
This theorem is referenced by: ssuni 4234 unipw 4667 opeluu 4688 unon 6690 limuni3 6711 uniinqs 7474 trcl 8243 rankwflemb 8295 ac5num 8498 dfac3 8583 isf34lem4 8838 axcclem 8918 ttukeylem7 8976 brdom7disj 8990 brdom6disj 8991 wrdexb 12722 dprdfeq0 17710 tgss2 20058 ppttop 20077 isclo 20158 neips 20184 2ndcomap 20528 2ndcsep 20529 locfincmp 20596 comppfsc 20602 txkgen 20722 txcon 20759 basqtop 20781 nrmr0reg 20819 alexsublem 21114 alexsubALTlem4 21120 alexsubALT 21121 ptcmplem4 21125 unirnblps 21489 unirnbl 21490 blbas 21500 met2ndci 21592 bndth 22041 dyadmbllem 22613 opnmbllem 22615 dya2iocnei 29154 dstfrvunirn 29357 pconcon 30004 cvmcov2 30048 cvmlift2lem11 30086 cvmlift2lem12 30087 neibastop2lem 31066 onint1 31159 icoreunrn 31808 opnmbllem0 32022 heibor1 32188 unichnidl 32310 prtlem16 32487 prter2 32499 truniALT 36947 unipwrVD 37269 unipwr 37270 truniALTVD 37316 unisnALT 37364 disjinfi 37522 stoweidlem43 38005 stoweidlem55 38017 salexct 38294 |
Copyright terms: Public domain | W3C validator |