| 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 4869 | . . 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 4868 |
| 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 4869 |
| This theorem is referenced by: eluni2 4872 elunii 4873 uniss 4876 eluniab 4882 uniun 4891 uniinOLD 4893 uni0 4897 unissb 4902 dfiun2g 4990 dftr2 5214 unipw 5422 dmuni 5895 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 21330 toprntopon 23043 isbasis2g 23066 tgval2 23074 ntreq0 23195 cmpsublem 23517 cmpsub 23518 cmpcld 23520 is1stc2 23560 alexsubALTlem3 24167 alexsubALT 24169 elold 28010 fnessref 36730 mh-infprim1bi 36919 bj-restuni 37599 difunieq 37880 ismnushort 44875 truniALT 45115 truniALTVD 45451 unisnALT 45499 uniclaxun 45560 elunif 45594 ssfiunibd 45886 stoweidlem27 46599 stoweidlem48 46620 setrec1lem3 50318 setrec1 50320 |
| Copyright terms: Public domain | W3C validator |