Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfiun2g | Structured version Visualization version GIF version |
Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) |
Ref | Expression |
---|---|
dfiun2g | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfra1 3219 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 | |
2 | rspa 3206 | . . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | |
3 | clel3g 3653 | . . . . . . 7 ⊢ (𝐵 ∈ 𝐶 → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) | |
4 | 2, 3 | syl 17 | . . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
5 | 1, 4 | rexbida 3318 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
6 | rexcom4 3249 | . . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)) | |
7 | 5, 6 | syl6bb 289 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
8 | r19.41v 3347 | . . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)) | |
9 | 8 | exbii 1844 | . . . . 5 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)) |
10 | exancom 1857 | . . . . 5 ⊢ (∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) | |
11 | 9, 10 | bitri 277 | . . . 4 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
12 | 7, 11 | syl6bb 289 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵))) |
13 | eliun 4922 | . . 3 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) | |
14 | eluniab 4852 | . . 3 ⊢ (𝑧 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) | |
15 | 12, 13, 14 | 3bitr4g 316 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑧 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) |
16 | 15 | eqrdv 2819 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∃wex 1776 ∈ wcel 2110 {cab 2799 ∀wral 3138 ∃wrex 3139 ∪ cuni 4837 ∪ ciun 4918 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-v 3496 df-uni 4838 df-iun 4920 |
This theorem is referenced by: dfiun2 4957 dfiun3g 5834 abnexg 7477 iunexg 7663 uniqs 8356 ac6num 9900 iunopn 21505 pnrmopn 21950 cncmp 21999 ptcmplem3 22661 iunmbl 24153 voliun 24154 sigaclcuni 31377 sigaclcu2 31379 sigaclci 31391 measvunilem 31471 meascnbl 31478 carsgclctunlem3 31578 uniqsALTV 35585 |
Copyright terms: Public domain | W3C validator |