| 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 3501 | . 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V) | |
| 2 | elex 3501 | . . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V) | |
| 3 | 2 | adantr 480 | . . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
| 4 | 3 | exlimiv 1930 | . 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V) |
| 5 | eleq1 2829 | . . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
| 6 | 5 | anbi1d 631 | . . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
| 7 | 6 | exbidv 1921 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
| 8 | df-uni 4908 | . . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)} | |
| 9 | 7, 8 | elab2g 3680 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))) |
| 10 | 1, 4, 9 | pm5.21nii 378 | 1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-uni 4908 |
| This theorem is referenced by: eluni2 4911 elunii 4912 uniss 4915 eluniab 4921 uniun 4930 uniin 4931 unissb 4939 unissbOLD 4940 dfiun2g 5030 dftr2 5261 unipw 5455 dmuni 5925 iotanul2 6531 fununi 6641 elunirn 7271 uniex2 7758 uniuni 7782 mpoxopxnop0 8240 fprresex 8335 wfrfunOLD 8359 wfrlem17OLD 8365 tfrlem7 8423 tfrlem9a 8426 inf2 9663 inf3lem2 9669 rankwflemb 9833 cardprclem 10019 carduni 10021 iunfictbso 10154 kmlem3 10193 kmlem4 10194 cfub 10289 isf34lem4 10417 grothtsk 10875 suplem1pr 11092 toprntopon 22931 isbasis2g 22955 tgval2 22963 ntreq0 23085 cmpsublem 23407 cmpsub 23408 cmpcld 23410 is1stc2 23450 alexsubALTlem3 24057 alexsubALT 24059 elold 27908 fnessref 36358 bj-restuni 37098 difunieq 37375 ismnushort 44320 truniALT 44561 truniALTVD 44898 unisnALT 44946 uniclaxun 45003 elunif 45021 ssfiunibd 45321 stoweidlem27 46042 stoweidlem48 46063 setrec1lem3 49208 setrec1 49210 |
| Copyright terms: Public domain | W3C validator |