![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eluniab | Structured version Visualization version GIF version |
Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.) |
Ref | Expression |
---|---|
eluniab | ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluni 4914 | . 2 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
2 | nfv 1911 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦 | |
3 | nfsab1 2719 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
4 | 2, 3 | nfan 1896 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) |
5 | nfv 1911 | . . 3 ⊢ Ⅎ𝑦(𝐴 ∈ 𝑥 ∧ 𝜑) | |
6 | eleq2w 2822 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥)) | |
7 | eleq1w 2821 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})) | |
8 | abid 2715 | . . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
9 | 7, 8 | bitrdi 287 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) |
10 | 6, 9 | anbi12d 632 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝑥 ∧ 𝜑))) |
11 | 4, 5, 10 | cbvexv1 2342 | . 2 ⊢ (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
12 | 1, 11 | bitri 275 | 1 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1775 ∈ wcel 2105 {cab 2711 ∪ cuni 4911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-uni 4912 |
This theorem is referenced by: elunirab 4926 dfiun2gOLD 5035 inuni 5355 elfv 6904 unielxp 8050 frrlem8 8316 frrlem10 8318 wfrlem12OLD 8358 tfrlem9 8423 dfac5lem2 10161 fin23lem30 10379 unisngl 23550 metrest 24552 aannenlem2 26385 fpwrelmapffslem 32749 dfiota3 35904 mptsnunlem 37320 nnoeomeqom 43301 |
Copyright terms: Public domain | W3C validator |