Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eluni | Structured version Visualization version GIF version |
Description: Membership in class union. (Contributed by NM, 22-May-1994.) |
Ref | Expression |
---|---|
eluni | ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3185 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3185 | . . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V) | |
3 | 2 | adantr 480 | . . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
4 | 3 | exlimiv 1845 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
5 | eleq1 2676 | . . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
6 | 5 | anbi1d 737 | . . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
7 | 6 | exbidv 1837 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
8 | df-uni 4373 | . . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)} | |
9 | 7, 8 | elab2g 3322 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
10 | 1, 4, 9 | pm5.21nii 367 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-uni 4373 |
This theorem is referenced by: eluni2 4376 elunii 4377 eluniab 4383 uniun 4392 uniin 4393 uniss 4394 unissb 4405 dftr2 4682 unipw 4845 dmuni 5256 fununi 5878 elunirn 6413 uniex2 6850 uniuni 6865 mpt2xopxnop0 7228 wfrfun 7312 wfrlem17 7318 tfrlem7 7366 tfrlem9a 7369 inf2 8403 inf3lem2 8409 rankwflemb 8539 cardprclem 8688 carduni 8690 iunfictbso 8820 kmlem3 8857 kmlem4 8858 cfub 8954 isf34lem4 9082 grothtsk 9536 suplem1pr 9753 isbasis2g 20563 tgval2 20571 ntreq0 20691 cmpsublem 21012 cmpsub 21013 cmpcld 21015 is1stc2 21055 alexsubALTlem3 21663 alexsubALT 21665 frrlem5c 31030 fnessref 31522 bj-restuni 32231 bj-toprntopon 32244 truniALT 37772 truniALTVD 38136 unisnALT 38184 elunif 38198 ssfiunibd 38464 stoweidlem27 38920 stoweidlem48 38941 setrec1lem3 42235 setrec1 42237 |
Copyright terms: Public domain | W3C validator |