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

Theorem fvelrn 6037
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 2527 . . . . 5  |-  ( x  =  A  ->  (
x  e.  dom  F  <->  A  e.  dom  F ) )
21anbi2d 715 . . . 4  |-  ( x  =  A  ->  (
( Fun  F  /\  x  e.  dom  F )  <-> 
( Fun  F  /\  A  e.  dom  F ) ) )
3 fveq2 5887 . . . . 5  |-  ( x  =  A  ->  ( F `  x )  =  ( F `  A ) )
43eleq1d 2523 . . . 4  |-  ( x  =  A  ->  (
( F `  x
)  e.  ran  F  <->  ( F `  A )  e.  ran  F ) )
52, 4imbi12d 326 . . 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 6016 . . . . 5  |-  ( ( Fun  F  /\  x  e.  dom  F )  ->  <. x ,  ( F `
 x ) >.  e.  F )
7 vex 3059 . . . . . 6  |-  x  e. 
_V
8 opeq1 4179 . . . . . . 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 3152 . . . . 5  |-  ( <.
x ,  ( F `
 x ) >.  e.  F  ->  E. y <. y ,  ( F `
 x ) >.  e.  F )
116, 10syl 17 . . . 4  |-  ( ( Fun  F  /\  x  e.  dom  F )  ->  E. y <. y ,  ( F `  x )
>.  e.  F )
12 fvex 5897 . . . . 5  |-  ( F `
 x )  e. 
_V
1312elrn2 5092 . . . 4  |-  ( ( F `  x )  e.  ran  F  <->  E. y <. y ,  ( F `
 x ) >.  e.  F )
1411, 13sylibr 217 . . 3  |-  ( ( Fun  F  /\  x  e.  dom  F )  -> 
( F `  x
)  e.  ran  F
)
155, 14vtoclg 3118 . 2  |-  ( A  e.  dom  F  -> 
( ( Fun  F  /\  A  e.  dom  F )  ->  ( F `  A )  e.  ran  F ) )
1615anabsi7 833 1  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( F `  A
)  e.  ran  F
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1454   E.wex 1673    e. wcel 1897   <.cop 3985   dom cdm 4852   ran crn 4853   Fun wfun 5594   ` cfv 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-iota 5564  df-fun 5602  df-fn 5603  df-fv 5608
This theorem is referenced by:  nelrnfvne  6038  fnfvelrn  6041  eldmrexrn  6050  fvn0fvelrn  6104  funfvima  6164  elunirn  6180  rankwflemb  8289  dfac9  8591  fin1a2lem6  8860  gsumpropd2lem  16564  usgraedg3  25161  nbgraf1olem5  25221  usgrwlknloop  25341  usgra2wlkspthlem2  25396  nvnencycllem  25419  wlkiswwlk1  25466  usg2wlkonot  25659  usg2wotspth  25660  opfv  28295  nofv  30592  sltres  30599  bdayelon  30617  nodenselem3  30620  bj-elccinfty  31700  bj-minftyccb  31711  icoreunrn  31806  indexdom  32105  diaclN  34662  dia1elN  34666  docaclN  34736  dibclN  34774  dfac21  35968  cncmpmax  37392  icccncfext  37802  stoweidlem27  37924  stoweidlem29  37926  stoweidlem29OLD  37927  stoweidlem59  37957  fourierdlem20  38026  fourierdlem63  38070  fourierdlem76  38083  fourierdlem82  38089  fourierdlem93  38100  fourierdlem113  38120  fge0iccico  38249  sge0sn  38258  sge0tsms  38259  sge0cl  38260  sge0isum  38306  hoicvr  38407  afvelrn  38707  usgredg3  39342  ushgredgedga  39355  ushgredgedgaloop  39357  subgruhgredgd  39405  edginwlk  39694  suppdm  40576
  Copyright terms: Public domain W3C validator