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 2723 | . 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V) | |
2 | elex 2723 | . . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) | |
3 | 2 | rexlimivw 2570 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V) |
4 | eleq1 2220 | . . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
5 | 4 | rexbidv 2458 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
6 | df-iun 3853 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
7 | 5, 6 | elab2g 2859 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
8 | 1, 3, 7 | pm5.21nii 694 | 1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1335 ∈ wcel 2128 ∃wrex 2436 Vcvv 2712 ∪ ciun 3851 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-rex 2441 df-v 2714 df-iun 3853 |
This theorem is referenced by: iuncom 3857 iuncom4 3858 iunconstm 3859 iuniin 3861 iunss1 3862 ss2iun 3866 dfiun2g 3883 ssiun 3893 ssiun2 3894 iunab 3897 iun0 3907 0iun 3908 iunn0m 3911 iunin2 3914 iundif2ss 3916 iindif2m 3918 iunxsng 3926 iunxsngf 3928 iunun 3929 iunxun 3930 iunxiun 3932 iunpwss 3942 disjiun 3962 triun 4077 iunpw 4442 xpiundi 4646 xpiundir 4647 iunxpf 4736 cnvuni 4774 dmiun 4797 dmuni 4798 rniun 4998 dfco2 5087 dfco2a 5088 coiun 5097 fun11iun 5437 imaiun 5712 eluniimadm 5717 opabex3d 6071 opabex3 6072 smoiun 6250 tfrlemi14d 6282 tfr1onlemres 6298 tfrcllemres 6311 fsum2dlemstep 11342 fisumcom2 11346 fsumiun 11385 fprod2dlemstep 11530 fprodcom2fi 11534 ennnfonelemrn 12218 ennnfonelemdm 12219 ctiunctlemf 12237 ctiunctlemfo 12238 |
Copyright terms: Public domain | W3C validator |