Theorem fniunfv 7183

Description: The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.)

Assertion

Ref	Expression
fniunfv	⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem fniunfv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6835	. . 3 ⊢ (𝐹‘𝑥) ∈ V
2	1	dfiun2 4982	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}
3		fnrnfv 6882	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
4	3	unieqd 4871	. 2 ⊢ (𝐹 Fn 𝐴 → ∪ ran 𝐹 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
5	2, 4	eqtr4id 2783	1 ⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹)

Syntax hints:   → wi 4   = wceq 1540  {cab 2707  ∃wrex 3053  ∪ cuni 4858  ∪ ciun 4941  ran crn 5620   Fn wfn 6477  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490

This theorem is referenced by:  funiunfv  7184  dffi3  9321  jech9.3  9710  hsmexlem5  10324  wuncval2  10641  dprdspan  19908  tgcmp  23286  txcmplem1  23526  txcmplem2  23527  xkococnlem  23544  alexsubALT  23936  bcth3  25229  ovolfioo  25366  ovolficc  25367  voliunlem2  25450  voliunlem3  25451  volsup  25455  uniiccdif  25477  uniioovol  25478  uniiccvol  25479  uniioombllem2  25482  uniioombllem4  25485  volsup2  25504  itg1climres  25613  itg2monolem1  25649  itg2gt0  25659  sigapildsys  34145  omssubadd  34284  carsgclctunlem3  34304  pibt2  37411  volsupnfl  37665  hbt  43123  ovolval4lem1  46650  ovolval5lem3  46655  ovnovollem1  46657  ovnovollem2  46658