![]() |
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 3493 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3493 | . . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V) | |
3 | 2 | adantr 482 | . . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
4 | 3 | exlimiv 1934 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
5 | eleq1 2822 | . . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
6 | 5 | anbi1d 631 | . . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
7 | 6 | exbidv 1925 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
8 | df-uni 4910 | . . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)} | |
9 | 7, 8 | elab2g 3671 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
10 | 1, 4, 9 | pm5.21nii 380 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 Vcvv 3475 ∪ cuni 4909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-uni 4910 |
This theorem is referenced by: eluni2 4913 elunii 4914 uniss 4917 eluniab 4924 uniun 4935 uniin 4936 unissb 4944 unissbOLD 4945 dfiun2g 5034 dftr2 5268 unipw 5451 dmuni 5915 iotanul2 6514 fununi 6624 elunirn 7250 uniex2 7728 uniuni 7749 mpoxopxnop0 8200 fprresex 8295 wfrfunOLD 8319 wfrlem17OLD 8325 tfrlem7 8383 tfrlem9a 8386 inf2 9618 inf3lem2 9624 rankwflemb 9788 cardprclem 9974 carduni 9976 iunfictbso 10109 kmlem3 10147 kmlem4 10148 cfub 10244 isf34lem4 10372 grothtsk 10830 suplem1pr 11047 toprntopon 22427 isbasis2g 22451 tgval2 22459 ntreq0 22581 cmpsublem 22903 cmpsub 22904 cmpcld 22906 is1stc2 22946 alexsubALTlem3 23553 alexsubALT 23555 elold 27364 fnessref 35242 bj-restuni 35978 difunieq 36255 ismnushort 43060 truniALT 43302 truniALTVD 43639 unisnALT 43687 elunif 43700 ssfiunibd 44019 stoweidlem27 44743 stoweidlem48 44764 setrec1lem3 47734 setrec1 47736 |
Copyright terms: Public domain | W3C validator |