![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eliun | Unicode version |
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.) |
Ref | Expression |
---|---|
eliun |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2566 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2566 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | rexlimivw 2429 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eleq1 2100 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | rexbidv 2327 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | df-iun 3659 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | elab2g 2689 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 3, 7 | pm5.21nii 620 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 df-rex 2312 df-v 2559 df-iun 3659 |
This theorem is referenced by: iuncom 3663 iuncom4 3664 iunconstm 3665 iuniin 3667 iunss1 3668 ss2iun 3672 dfiun2g 3689 ssiun 3699 ssiun2 3700 iunab 3703 iun0 3713 0iun 3714 iunn0m 3717 iunin2 3720 iundif2ss 3722 iindif2m 3724 iunxsng 3732 iunun 3734 iunxun 3735 iunxiun 3736 iunpwss 3743 triun 3867 iunpw 4211 xpiundi 4398 xpiundir 4399 iunxpf 4484 cnvuni 4521 dmiun 4544 dmuni 4545 rniun 4734 dfco2 4820 dfco2a 4821 coiun 4830 fun11iun 5147 imaiun 5399 eluniimadm 5404 opabex3d 5748 opabex3 5749 smoiun 5916 tfrlemi14d 5947 |
Copyright terms: Public domain | W3C validator |