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

Theorem imaiun 7192
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 3271 . . . 4 (∃𝑥𝐵𝑧(𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑧𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
2 vex 3449 . . . . . 6 𝑦 ∈ V
32elima3 6020 . . . . 5 (𝑦 ∈ (𝐴𝐶) ↔ ∃𝑧(𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
43rexbii 3097 . . . 4 (∃𝑥𝐵 𝑦 ∈ (𝐴𝐶) ↔ ∃𝑥𝐵𝑧(𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
5 eliun 4958 . . . . . . 7 (𝑧 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑧𝐶)
65anbi1i 624 . . . . . 6 ((𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (∃𝑥𝐵 𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
7 r19.41v 3185 . . . . . 6 (∃𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (∃𝑥𝐵 𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
86, 7bitr4i 277 . . . . 5 ((𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
98exbii 1850 . . . 4 (∃𝑧(𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑧𝑥𝐵 (𝑧𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
101, 4, 93bitr4ri 303 . . 3 (∃𝑧(𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑥𝐵 𝑦 ∈ (𝐴𝐶))
112elima3 6020 . . 3 (𝑦 ∈ (𝐴 𝑥𝐵 𝐶) ↔ ∃𝑧(𝑧 𝑥𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
12 eliun 4958 . . 3 (𝑦 𝑥𝐵 (𝐴𝐶) ↔ ∃𝑥𝐵 𝑦 ∈ (𝐴𝐶))
1310, 11, 123bitr4i 302 . 2 (𝑦 ∈ (𝐴 𝑥𝐵 𝐶) ↔ 𝑦 𝑥𝐵 (𝐴𝐶))
1413eqriv 2733 1 (𝐴 𝑥𝐵 𝐶) = 𝑥𝐵 (𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wex 1781  wcel 2106  wrex 3073  cop 4592   ciun 4954  cima 5636
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-iun 4956  df-br 5106  df-opab 5168  df-xp 5639  df-cnv 5641  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646
This theorem is referenced by:  imauni  7193  uniqs  8716  hsmexlem4  10365  hsmexlem5  10366  xkococnlem  23010  ismbf3d  25018  mbfimaopnlem  25019  i1fima  25042  i1fd  25045  itg1addlem5  25065  limciun  25258  sibfof  32940  eulerpartlemgh  32978  poimirlem30  36108  itg2addnclem2  36130  ftc1anclem6  36156  uniqsALTV  36790  smfresal  45019
  Copyright terms: Public domain W3C validator