| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > eliin | Unicode version | ||
| Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.) |
| Ref | Expression |
|---|---|
| eliin |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 2268 |
. . 3
| |
| 2 | 1 | ralbidv 2506 |
. 2
|
| 3 | df-iin 3930 |
. 2
| |
| 4 | 2, 3 | elab2g 2920 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-v 2774 df-iin 3930 |
| This theorem is referenced by: iinconstm 3936 iuniin 3937 iinss1 3939 ssiinf 3977 iinss 3979 iinss2 3980 iinab 3989 iundif2ss 3993 iindif2m 3995 iinin2m 3996 elriin 3998 iinpw 4018 xpiindim 4815 cnviinm 5224 iinerm 6694 ixpiinm 6811 |
| Copyright terms: Public domain | W3C validator |