![]() |
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 4908 | . . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)} | |
9 | 7, 8 | elab2g 3669 | . 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 4907 |
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 4908 |
This theorem is referenced by: eluni2 4911 elunii 4912 uniss 4915 eluniab 4922 uniun 4933 uniin 4934 unissb 4942 unissbOLD 4943 dfiun2g 5032 dftr2 5266 unipw 5449 dmuni 5912 iotanul2 6510 fununi 6620 elunirn 7245 uniex2 7723 uniuni 7744 mpoxopxnop0 8195 fprresex 8290 wfrfunOLD 8314 wfrlem17OLD 8320 tfrlem7 8378 tfrlem9a 8381 inf2 9614 inf3lem2 9620 rankwflemb 9784 cardprclem 9970 carduni 9972 iunfictbso 10105 kmlem3 10143 kmlem4 10144 cfub 10240 isf34lem4 10368 grothtsk 10826 suplem1pr 11043 toprntopon 22409 isbasis2g 22433 tgval2 22441 ntreq0 22563 cmpsublem 22885 cmpsub 22886 cmpcld 22888 is1stc2 22928 alexsubALTlem3 23535 alexsubALT 23537 elold 27344 fnessref 35180 bj-restuni 35916 difunieq 36193 ismnushort 42993 truniALT 43235 truniALTVD 43572 unisnALT 43620 elunif 43633 ssfiunibd 43954 stoweidlem27 44678 stoweidlem48 44699 setrec1lem3 47636 setrec1 47638 |
Copyright terms: Public domain | W3C validator |