Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaiun Structured version   Visualization version   GIF version

Theorem imaiun 6996
 Description: The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
imaiun (𝐴 𝑥𝐵 𝐶) = 𝑥𝐵 (𝐴𝐶)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem imaiun
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rexcom4 3177 . . . 4 (∃𝑥𝐵𝑧(𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑧𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
2 vex 3413 . . . . . 6 𝑦 ∈ V
32elima3 5908 . . . . 5 (𝑦 ∈ (𝐴𝐶) ↔ ∃𝑧(𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
43rexbii 3175 . . . 4 (∃𝑥𝐵 𝑦 ∈ (𝐴𝐶) ↔ ∃𝑥𝐵𝑧(𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
5 eliun 4887 . . . . . . 7 (𝑧 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑧𝐶)
65anbi1i 626 . . . . . 6 ((𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (∃𝑥𝐵 𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
7 r19.41v 3265 . . . . . 6 (∃𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (∃𝑥𝐵 𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
86, 7bitr4i 281 . . . . 5 ((𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
98exbii 1849 . . . 4 (∃𝑧(𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑧𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
101, 4, 93bitr4ri 307 . . 3 (∃𝑧(𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑥𝐵 𝑦 ∈ (𝐴𝐶))
112elima3 5908 . . 3 (𝑦 ∈ (𝐴 𝑥𝐵 𝐶) ↔ ∃𝑧(𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
12 eliun 4887 . . 3 (𝑦 𝑥𝐵 (𝐴𝐶) ↔ ∃𝑥𝐵 𝑦 ∈ (𝐴𝐶))
1310, 11, 123bitr4i 306 . 2 (𝑦 ∈ (𝐴 𝑥𝐵 𝐶) ↔ 𝑦 𝑥𝐵 (𝐴𝐶))
1413eqriv 2755 1 (𝐴 𝑥𝐵 𝐶) = 𝑥𝐵 (𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃wrex 3071  ⟨cop 4528  ∪ ciun 4883   “ cima 5527 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-iun 4885  df-br 5033  df-opab 5095  df-xp 5530  df-cnv 5532  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537 This theorem is referenced by:  imauni  6997  uniqs  8367  hsmexlem4  9889  hsmexlem5  9890  xkococnlem  22359  ismbf3d  24354  mbfimaopnlem  24355  i1fima  24378  i1fd  24381  itg1addlem5  24400  limciun  24593  sibfof  31826  eulerpartlemgh  31864  poimirlem30  35367  itg2addnclem2  35389  ftc1anclem6  35415  uniqsALTV  36026  smfresal  43786
 Copyright terms: Public domain W3C validator