![]() |
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 3461 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V) | |
2 | elex 3461 | . . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V) | |
3 | 2 | adantr 481 | . . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
4 | 3 | exlimiv 1933 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
5 | eleq1 2825 | . . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
6 | 5 | anbi1d 630 | . . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
7 | 6 | exbidv 1924 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
8 | df-uni 4864 | . . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)} | |
9 | 7, 8 | elab2g 3630 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
10 | 1, 4, 9 | pm5.21nii 379 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 Vcvv 3443 ∪ cuni 4863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 df-uni 4864 |
This theorem is referenced by: eluni2 4867 elunii 4868 uniss 4871 eluniab 4878 uniun 4889 uniin 4890 unissb 4898 unissbOLD 4899 dfiun2g 4988 dftr2 5222 unipw 5405 dmuni 5868 iotanul2 6463 fununi 6573 elunirn 7194 uniex2 7671 uniuni 7692 mpoxopxnop0 8142 fprresex 8237 wfrfunOLD 8261 wfrlem17OLD 8267 tfrlem7 8325 tfrlem9a 8328 inf2 9555 inf3lem2 9561 rankwflemb 9725 cardprclem 9911 carduni 9913 iunfictbso 10046 kmlem3 10084 kmlem4 10085 cfub 10181 isf34lem4 10309 grothtsk 10767 suplem1pr 10984 toprntopon 22258 isbasis2g 22282 tgval2 22290 ntreq0 22412 cmpsublem 22734 cmpsub 22735 cmpcld 22737 is1stc2 22777 alexsubALTlem3 23384 alexsubALT 23386 elold 27183 fnessref 34796 bj-restuni 35535 difunieq 35812 ismnushort 42523 truniALT 42765 truniALTVD 43102 unisnALT 43150 elunif 43163 ssfiunibd 43479 stoweidlem27 44200 stoweidlem48 44221 setrec1lem3 47066 setrec1 47068 |
Copyright terms: Public domain | W3C validator |