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

Theorem fniunfv 7000
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.
StepHypRef Expression
1 fnrnfv 6722 . . 3 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
21unieqd 4847 . 2 (𝐹 Fn 𝐴 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
3 fvex 6680 . . 3 (𝐹𝑥) ∈ V
43dfiun2 4955 . 2 𝑥𝐴 (𝐹𝑥) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)}
52, 4syl6reqr 2880 1 (𝐹 Fn 𝐴 𝑥𝐴 (𝐹𝑥) = ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  {cab 2804  wrex 3144   cuni 4837   ciun 4917  ran crn 5555   Fn wfn 6347  cfv 6352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6312  df-fun 6354  df-fn 6355  df-fv 6360
This theorem is referenced by:  funiunfv  7001  dffi3  8884  jech9.3  9232  hsmexlem5  9841  wuncval2  10158  dprdspan  19069  tgcmp  21928  txcmplem1  22168  txcmplem2  22169  xkococnlem  22186  alexsubALT  22578  bcth3  23852  ovolfioo  23986  ovolficc  23987  voliunlem2  24070  voliunlem3  24071  volsup  24075  uniiccdif  24097  uniioovol  24098  uniiccvol  24099  uniioombllem2  24102  uniioombllem4  24105  volsup2  24124  itg1climres  24233  itg2monolem1  24269  itg2gt0  24279  sigapildsys  31310  omssubadd  31447  carsgclctunlem3  31467  dftrpred2  32945  pibt2  34570  volsupnfl  34807  hbt  39598  ovolval4lem1  42800  ovolval5lem3  42805  ovnovollem1  42807  ovnovollem2  42808
  Copyright terms: Public domain W3C validator