![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunab | Structured version Visualization version GIF version |
Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.) |
Ref | Expression |
---|---|
iunab | ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2902 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
2 | nfab1 2904 | . . . 4 ⊢ Ⅎ𝑦{𝑦 ∣ 𝜑} | |
3 | 1, 2 | nfiun 5027 | . . 3 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} |
4 | nfab1 2904 | . . 3 ⊢ Ⅎ𝑦{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} | |
5 | 3, 4 | cleqf 2931 | . 2 ⊢ (∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ↔ 𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑})) |
6 | abid 2715 | . . . 4 ⊢ (𝑦 ∈ {𝑦 ∣ 𝜑} ↔ 𝜑) | |
7 | 6 | rexbii 3091 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑦 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) |
8 | eliun 4999 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑦 ∣ 𝜑}) | |
9 | abid 2715 | . . 3 ⊢ (𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑) | |
10 | 7, 8, 9 | 3bitr4i 303 | . 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ↔ 𝑦 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}) |
11 | 5, 10 | mpgbir 1795 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 = wceq 1536 ∈ wcel 2105 {cab 2711 ∃wrex 3067 ∪ ciun 4995 |
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-nfc 2889 df-ral 3059 df-rex 3068 df-v 3479 df-iun 4997 |
This theorem is referenced by: iunrab 5056 iunidOLD 5065 dfimafn2 6971 pzriprnglem10 21518 pzriprnglem11 21519 rabiun 37579 dfaimafn2 47115 rnfdmpr 47230 |
Copyright terms: Public domain | W3C validator |