Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eliin | Structured version Visualization version Unicode version |
Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.) |
Ref | Expression |
---|---|
eliin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2689 | . . 3 | |
2 | 1 | ralbidv 2986 | . 2 |
3 | df-iin 4523 | . 2 | |
4 | 2, 3 | elab2g 3353 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wcel 1990 wral 2912 ciin 4521 |
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-ral 2917 df-v 3202 df-iin 4523 |
This theorem is referenced by: iinconst 4530 iuniin 4531 iinss1 4533 ssiinf 4569 iinss 4571 iinss2 4572 iinab 4581 iinun2 4586 iundif2 4587 iindif2 4589 iinin2 4590 elriin 4593 iinpw 4617 xpiindi 5257 cnviin 5672 iinpreima 6345 iiner 7819 ixpiin 7934 boxriin 7950 iunocv 20025 hauscmplem 21209 txtube 21443 isfcls 21813 iscmet3 23091 taylfval 24113 iinssiun 29377 fnemeet1 32361 diaglbN 36344 dibglbN 36455 dihglbcpreN 36589 kelac1 37633 eliind 39240 eliuniin 39279 eliin2f 39287 eliinid 39294 eliuniin2 39303 iinssiin 39312 eliind2 39313 iinssf 39327 allbutfi 39616 meaiininclem 40700 hspdifhsp 40830 iinhoiicclem 40887 preimageiingt 40930 preimaleiinlt 40931 smflimlem2 40980 smflimsuplem5 41030 smflimsuplem7 41032 |
Copyright terms: Public domain | W3C validator |