| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iunrab | Structured version Visualization version GIF version | ||
| Description: The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
| Ref | Expression |
|---|---|
| iunrab | ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iunab 5051 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)} | |
| 2 | df-rab 3437 | . . . 4 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)} | |
| 3 | 2 | a1i 11 | . . 3 ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)}) |
| 4 | 3 | iuneq2i 5013 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)} |
| 5 | df-rab 3437 | . . 3 ⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)} | |
| 6 | r19.42v 3191 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)) | |
| 7 | 6 | abbii 2809 | . . 3 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)} |
| 8 | 5, 7 | eqtr4i 2768 | . 2 ⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)} |
| 9 | 1, 4, 8 | 3eqtr4i 2775 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∈ wcel 2108 {cab 2714 ∃wrex 3070 {crab 3436 ∪ ciun 4991 |
| 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-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-ss 3968 df-iun 4993 |
| This theorem is referenced by: hashrabrex 15861 incexc2 15874 phisum 16828 itg2monolem1 25785 aannenlem1 26370 musum 27234 lgsquadlem1 27424 lgsquadlem2 27425 edglnl 29160 rabrexfi 32525 iunpreima 32577 poimirlem27 37654 cnambfre 37675 mapdval3N 41633 mapdval5N 41635 fiphp3d 42830 |
| Copyright terms: Public domain | W3C validator |