| 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 4910 | . 2 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})) | |
| 2 | nfv 1914 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦 | |
| 3 | nfsab1 2722 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
| 4 | 2, 3 | nfan 1899 | . . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) |
| 5 | nfv 1914 | . . 3 ⊢ Ⅎ𝑦(𝐴 ∈ 𝑥 ∧ 𝜑) | |
| 6 | eleq2w 2825 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥)) | |
| 7 | eleq1w 2824 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})) | |
| 8 | abid 2718 | . . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
| 9 | 7, 8 | bitrdi 287 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) |
| 10 | 6, 9 | anbi12d 632 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝑥 ∧ 𝜑))) |
| 11 | 4, 5, 10 | cbvexv1 2344 | . 2 ⊢ (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
| 12 | 1, 11 | bitri 275 | 1 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 {cab 2714 ∪ 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-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-uni 4908 |
| This theorem is referenced by: elunirab 4922 dfiun2gOLD 5031 inuni 5350 elfv 6904 unielxp 8052 frrlem8 8318 frrlem10 8320 wfrlem12OLD 8360 tfrlem9 8425 dfac5lem2 10164 fin23lem30 10382 unisngl 23535 metrest 24537 aannenlem2 26371 fpwrelmapffslem 32743 dfiota3 35924 mptsnunlem 37339 nnoeomeqom 43325 |
| Copyright terms: Public domain | W3C validator |