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

Theorem fniunfv 6066
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  |-  ( F  Fn  A  ->  U_ x  e.  A  ( F `  x )  =  U. ran  F )
Distinct variable groups:    x, A    x, F

Proof of Theorem fniunfv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 fnrnfv 5840 . . 3  |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
21unieqd 4202 . 2  |-  ( F  Fn  A  ->  U. ran  F  =  U. { y  |  E. x  e.  A  y  =  ( F `  x ) } )
3 fvex 5802 . . 3  |-  ( F `
 x )  e. 
_V
43dfiun2 4305 . 2  |-  U_ x  e.  A  ( F `  x )  =  U. { y  |  E. x  e.  A  y  =  ( F `  x ) }
52, 4syl6reqr 2511 1  |-  ( F  Fn  A  ->  U_ x  e.  A  ( F `  x )  =  U. ran  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   {cab 2436   E.wrex 2796   U.cuni 4192   U_ciun 4272   ran crn 4942    Fn wfn 5514   ` cfv 5519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-iota 5482  df-fun 5521  df-fn 5522  df-fv 5527
This theorem is referenced by:  funiunfv  6067  dffi3  7785  jech9.3  8125  hsmexlem5  8703  wuncval2  9018  dprdspan  16638  tgcmp  19129  txcmplem1  19339  txcmplem2  19340  xkococnlem  19357  alexsubALT  19748  bcth3  20967  ovolfioo  21076  ovolficc  21077  voliunlem2  21158  voliunlem3  21159  volsup  21163  uniiccdif  21184  uniioovol  21185  uniiccvol  21186  uniioombllem2  21189  uniioombllem4  21192  volsup2  21211  itg1climres  21318  itg2monolem1  21354  itg2gt0  21364  dftrpred2  27820  volsupnfl  28577  hbt  29627
  Copyright terms: Public domain W3C validator