Theorem imaiun 7196

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.

Step	Hyp	Ref	Expression
1		rexcom4 3267	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 ∃𝑧(𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑧∃𝑥 ∈ 𝐵 (𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
2		vex 3436	. . . . . 6 ⊢ 𝑦 ∈ V
3	2	elima3 6026	. . . . 5 ⊢ (𝑦 ∈ (𝐴 “ 𝐶) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
4	3	rexbii 3087	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 “ 𝐶) ↔ ∃𝑥 ∈ 𝐵 ∃𝑧(𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
5		eliun 4932	. . . . . . 7 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑧 ∈ 𝐶)
6	5	anbi1i 630	. . . . . 6 ⊢ ((𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
7		r19.41v 3170	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐵 (𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
8	6, 7	bitr4i 279	. . . . 5 ⊢ ((𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐵 (𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
9	8	exbii 1855	. . . 4 ⊢ (∃𝑧(𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑧∃𝑥 ∈ 𝐵 (𝑧 ∈ 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
10	1, 4, 9	3bitr4ri 305	. . 3 ⊢ (∃𝑧(𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 “ 𝐶))
11	2	elima3 6026	. . 3 ⊢ (𝑦 ∈ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ ∃𝑧(𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ⟨𝑧, 𝑦⟩ ∈ 𝐴))
12		eliun 4932	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶) ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 “ 𝐶))
13	10, 11, 12	3bitr4i 304	. 2 ⊢ (𝑦 ∈ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶))
14	13	eqriv 2737	1 ⊢ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶)

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064  ⟨cop 4568  ∪ ciun 4928   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-11 2168  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-iun 4930  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  imauni  7197  uniqs  8717  hsmexlem4  10349  hsmexlem5  10350  xkococnlem  23649  ismbf3d  25646  mbfimaopnlem  25647  i1fima  25670  i1fd  25673  itg1addlem5  25692  limciun  25886  sibfof  34531  eulerpartlemgh  34569  poimirlem30  38024  itg2addnclem2  38046  ftc1anclem6  38072  smfresal  47238