![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eliun | GIF version |
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.) |
Ref | Expression |
---|---|
eliun | ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2644 | . 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V) | |
2 | elex 2644 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | rexlimivw 2498 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V) |
4 | eleq1 2157 | . . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
5 | 4 | rexbidv 2392 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
6 | df-iun 3754 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
7 | 5, 6 | elab2g 2776 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
8 | 1, 3, 7 | pm5.21nii 658 | 1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1296 ∈ wcel 1445 ∃wrex 2371 Vcvv 2633 ∪ ciun 3752 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-rex 2376 df-v 2635 df-iun 3754 |
This theorem is referenced by: iuncom 3758 iuncom4 3759 iunconstm 3760 iuniin 3762 iunss1 3763 ss2iun 3767 dfiun2g 3784 ssiun 3794 ssiun2 3795 iunab 3798 iun0 3808 0iun 3809 iunn0m 3812 iunin2 3815 iundif2ss 3817 iindif2m 3819 iunxsng 3827 iunxsngf 3829 iunun 3830 iunxun 3831 iunxiun 3832 iunpwss 3842 disjiun 3862 triun 3971 iunpw 4330 xpiundi 4525 xpiundir 4526 iunxpf 4615 cnvuni 4653 dmiun 4676 dmuni 4677 rniun 4875 dfco2 4964 dfco2a 4965 coiun 4974 fun11iun 5309 imaiun 5577 eluniimadm 5582 opabex3d 5930 opabex3 5931 smoiun 6104 tfrlemi14d 6136 tfr1onlemres 6152 tfrcllemres 6165 fsum2dlemstep 10977 fisumcom2 10981 fsumiun 11020 |
Copyright terms: Public domain | W3C validator |