| 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 3478 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V) | |
| 2 | elex 3478 | . . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V) | |
| 3 | 2 | adantr 485 | . . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
| 4 | 3 | exlimiv 1953 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
| 5 | eleq1 2853 | . . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
| 6 | 5 | anbi1d 642 | . . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
| 7 | 6 | exbidv 1944 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
| 8 | df-uni 4868 | . . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)} | |
| 9 | 7, 8 | elab2g 3642 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
| 10 | 1, 4, 9 | pm5.21nii 381 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 209 ∧ wa 400 = wceq 1563 ∃wex 1802 ∈ wcel 2145 Vcvv 3457 ∪ cuni 4867 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-tru 1566 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-v 3459 df-uni 4868 |
| This theorem is referenced by: eluni2 4871 elunii 4872 uniss 4875 eluniab 4881 uniun 4890 uniinOLD 4892 uni0 4896 unissb 4901 dfiun2g 4989 dftr2 5213 unipw 5421 dmuni 5894 iotanul2 6498 fununi 6600 elunirn 7239 uniex2 7725 uniuni 7749 mpoxopxnop0 8199 fprresex 8295 tfrlem7 8358 tfrlem9a 8361 inf2 9580 inf3lem2 9586 rankwflemb 9753 cardprclem 9953 carduni 9955 iunfictbso 10086 kmlem3 10124 kmlem4 10125 cfub 10220 isf34lem4 10349 grothtsk 10808 suplem1pr 11025 lidlunin0 21327 toprntopon 23039 isbasis2g 23062 tgval2 23070 ntreq0 23191 cmpsublem 23513 cmpsub 23514 cmpcld 23516 is1stc2 23556 alexsubALTlem3 24163 alexsubALT 24165 elold 28006 fnessref 36725 mh-infprim1bi 36914 bj-restuni 37594 difunieq 37875 ismnushort 44870 truniALT 45109 truniALTVD 45445 unisnALT 45493 uniclaxun 45554 elunif 45595 ssfiunibd 45887 stoweidlem27 46600 stoweidlem48 46621 setrec1lem3 50319 setrec1 50321 |
| Copyright terms: Public domain | W3C validator |