![]() |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 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 7667 uniuni 7688 mpoxopxnop0 8138 fprresex 8233 wfrfunOLD 8257 wfrlem17OLD 8263 tfrlem7 8321 tfrlem9a 8324 inf2 9517 inf3lem2 9523 rankwflemb 9687 cardprclem 9873 carduni 9875 iunfictbso 10008 kmlem3 10046 kmlem4 10047 cfub 10143 isf34lem4 10271 grothtsk 10729 suplem1pr 10946 toprntopon 22226 isbasis2g 22250 tgval2 22258 ntreq0 22380 cmpsublem 22702 cmpsub 22703 cmpcld 22705 is1stc2 22745 alexsubALTlem3 23352 alexsubALT 23354 elold 27151 fnessref 34767 bj-restuni 35506 difunieq 35783 ismnushort 42492 truniALT 42734 truniALTVD 43071 unisnALT 43119 elunif 43132 ssfiunibd 43448 stoweidlem27 44169 stoweidlem48 44190 setrec1lem3 47035 setrec1 47037 |
Copyright terms: Public domain | W3C validator |