| 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 4866 | . 2 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
| 2 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦 | |
| 3 | nfsab1 2722 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
| 4 | 2, 3 | nfan 1900 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) |
| 5 | nfv 1915 | . . 3 ⊢ Ⅎ𝑦(𝐴 ∈ 𝑥 ∧ 𝜑) | |
| 6 | eleq2w 2820 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥)) | |
| 7 | eleq1w 2819 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})) | |
| 8 | abid 2718 | . . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
| 9 | 7, 8 | bitrdi 287 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) |
| 10 | 6, 9 | anbi12d 632 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝑥 ∧ 𝜑))) |
| 11 | 4, 5, 10 | cbvexv1 2346 | . 2 ⊢ (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
| 12 | 1, 11 | bitri 275 | 1 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1780 ∈ wcel 2113 {cab 2714 ∪ cuni 4863 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1544 df-ex 1781 df-nf 1785 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-v 3442 df-uni 4864 |
| This theorem is referenced by: elunirab 4878 inuni 5295 elfv 6832 unielxp 7971 frrlem8 8235 frrlem10 8237 tfrlem9 8316 dfac5lem2 10034 fin23lem30 10252 unisngl 23471 metrest 24468 aannenlem2 26293 fpwrelmapffslem 32811 dfiota3 36115 mptsnunlem 37543 nnoeomeqom 43554 |
| Copyright terms: Public domain | W3C validator |