| 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 4861 | . 2 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
| 2 | nfv 1914 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦 | |
| 3 | nfsab1 2715 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
| 4 | 2, 3 | nfan 1899 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) |
| 5 | nfv 1914 | . . 3 ⊢ Ⅎ𝑦(𝐴 ∈ 𝑥 ∧ 𝜑) | |
| 6 | eleq2w 2812 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥)) | |
| 7 | eleq1w 2811 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})) | |
| 8 | abid 2711 | . . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
| 9 | 7, 8 | bitrdi 287 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) |
| 10 | 6, 9 | anbi12d 632 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝑥 ∧ 𝜑))) |
| 11 | 4, 5, 10 | cbvexv1 2340 | . 2 ⊢ (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
| 12 | 1, 11 | bitri 275 | 1 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2109 {cab 2707 ∪ cuni 4858 |
| 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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-v 3438 df-uni 4859 |
| This theorem is referenced by: elunirab 4873 inuni 5289 elfv 6820 unielxp 7962 frrlem8 8226 frrlem10 8228 tfrlem9 8307 dfac5lem2 10018 fin23lem30 10236 unisngl 23412 metrest 24410 aannenlem2 26235 fpwrelmapffslem 32675 dfiota3 35897 mptsnunlem 37312 nnoeomeqom 43285 |
| Copyright terms: Public domain | W3C validator |