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 2741 | . 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V) | |
2 | elex 2741 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | rexlimivw 2583 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V) |
4 | eleq1 2233 | . . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
5 | 4 | rexbidv 2471 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
6 | df-iun 3875 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
7 | 5, 6 | elab2g 2877 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
8 | 1, 3, 7 | pm5.21nii 699 | 1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1348 ∈ wcel 2141 ∃wrex 2449 Vcvv 2730 ∪ ciun 3873 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-v 2732 df-iun 3875 |
This theorem is referenced by: iuncom 3879 iuncom4 3880 iunconstm 3881 iuniin 3883 iunss1 3884 ss2iun 3888 dfiun2g 3905 ssiun 3915 ssiun2 3916 iunab 3919 iun0 3929 0iun 3930 iunn0m 3933 iunin2 3936 iundif2ss 3938 iindif2m 3940 iunxsng 3948 iunxsngf 3950 iunun 3951 iunxun 3952 iunxiun 3954 iunpwss 3964 disjiun 3984 triun 4100 iunpw 4465 xpiundi 4669 xpiundir 4670 iunxpf 4759 cnvuni 4797 dmiun 4820 dmuni 4821 rniun 5021 dfco2 5110 dfco2a 5111 coiun 5120 fun11iun 5463 imaiun 5739 eluniimadm 5744 opabex3d 6100 opabex3 6101 smoiun 6280 tfrlemi14d 6312 tfr1onlemres 6328 tfrcllemres 6341 fsum2dlemstep 11397 fisumcom2 11401 fsumiun 11440 fprod2dlemstep 11585 fprodcom2fi 11589 ennnfonelemrn 12374 ennnfonelemdm 12375 ctiunctlemf 12393 ctiunctlemfo 12394 |
Copyright terms: Public domain | W3C validator |