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

Theorem fvelrn 6000
Description: A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
Assertion
Ref Expression
fvelrn  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( F `  A
)  e.  ran  F
)

Proof of Theorem fvelrn
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2526 . . . . 5  |-  ( x  =  A  ->  (
x  e.  dom  F  <->  A  e.  dom  F ) )
21anbi2d 701 . . . 4  |-  ( x  =  A  ->  (
( Fun  F  /\  x  e.  dom  F )  <-> 
( Fun  F  /\  A  e.  dom  F ) ) )
3 fveq2 5848 . . . . 5  |-  ( x  =  A  ->  ( F `  x )  =  ( F `  A ) )
43eleq1d 2523 . . . 4  |-  ( x  =  A  ->  (
( F `  x
)  e.  ran  F  <->  ( F `  A )  e.  ran  F ) )
52, 4imbi12d 318 . . 3  |-  ( x  =  A  ->  (
( ( Fun  F  /\  x  e.  dom  F )  ->  ( F `  x )  e.  ran  F )  <->  ( ( Fun 
F  /\  A  e.  dom  F )  ->  ( F `  A )  e.  ran  F ) ) )
6 funfvop 5975 . . . . 5  |-  ( ( Fun  F  /\  x  e.  dom  F )  ->  <. x ,  ( F `
 x ) >.  e.  F )
7 vex 3109 . . . . . 6  |-  x  e. 
_V
8 opeq1 4203 . . . . . . 7  |-  ( y  =  x  ->  <. y ,  ( F `  x ) >.  =  <. x ,  ( F `  x ) >. )
98eleq1d 2523 . . . . . 6  |-  ( y  =  x  ->  ( <. y ,  ( F `
 x ) >.  e.  F  <->  <. x ,  ( F `  x )
>.  e.  F ) )
107, 9spcev 3198 . . . . 5  |-  ( <.
x ,  ( F `
 x ) >.  e.  F  ->  E. y <. y ,  ( F `
 x ) >.  e.  F )
116, 10syl 16 . . . 4  |-  ( ( Fun  F  /\  x  e.  dom  F )  ->  E. y <. y ,  ( F `  x )
>.  e.  F )
12 fvex 5858 . . . . 5  |-  ( F `
 x )  e. 
_V
1312elrn2 5231 . . . 4  |-  ( ( F `  x )  e.  ran  F  <->  E. y <. y ,  ( F `
 x ) >.  e.  F )
1411, 13sylibr 212 . . 3  |-  ( ( Fun  F  /\  x  e.  dom  F )  -> 
( F `  x
)  e.  ran  F
)
155, 14vtoclg 3164 . 2  |-  ( A  e.  dom  F  -> 
( ( Fun  F  /\  A  e.  dom  F )  ->  ( F `  A )  e.  ran  F ) )
1615anabsi7 817 1  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( F `  A
)  e.  ran  F
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398   E.wex 1617    e. wcel 1823   <.cop 4022   dom cdm 4988   ran crn 4989   Fun wfun 5564   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-iota 5534  df-fun 5572  df-fn 5573  df-fv 5578
This theorem is referenced by:  nelrnfvne  6001  fnfvelrn  6004  eldmrexrn  6013  fvn0fvelrn  6064  funfvima  6122  elunirn  6138  rankwflemb  8202  dfac9  8507  fin1a2lem6  8776  gsumpropd2lem  16099  usgraedg3  24588  nbgraf1olem5  24647  usgrnloop  24767  usgra2wlkspthlem2  24822  nvnencycllem  24845  wlkiswwlk1  24892  usg2wlkonot  25085  usg2wotspth  25086  opfv  27707  nofv  29657  sltres  29664  bdayelon  29680  nodenselem3  29683  indexdom  30465  dfac21  31251  cncmpmax  31647  icccncfext  31929  stoweidlem27  32048  stoweidlem29  32050  stoweidlem59  32080  fourierdlem20  32148  fourierdlem63  32191  fourierdlem76  32204  fourierdlem82  32210  fourierdlem93  32221  fourierdlem113  32241  afvelrn  32492  suppdm  33366  bj-elccinfty  35017  bj-minftyccb  35028  diaclN  37174  dia1elN  37178  docaclN  37248  dibclN  37286
  Copyright terms: Public domain W3C validator