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

Theorem fvelrn 6843
 Description: A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
Assertion
Ref Expression
fvelrn ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)

Proof of Theorem fvelrn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2900 . . . . 5 (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹𝐴 ∈ dom 𝐹))
21anbi2d 630 . . . 4 (𝑥 = 𝐴 → ((Fun 𝐹𝑥 ∈ dom 𝐹) ↔ (Fun 𝐹𝐴 ∈ dom 𝐹)))
3 fveq2 6669 . . . . 5 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
43eleq1d 2897 . . . 4 (𝑥 = 𝐴 → ((𝐹𝑥) ∈ ran 𝐹 ↔ (𝐹𝐴) ∈ ran 𝐹))
52, 4imbi12d 347 . . 3 (𝑥 = 𝐴 → (((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹) ↔ ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)))
6 funfvop 6819 . . . . 5 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹)
7 vex 3497 . . . . . 6 𝑥 ∈ V
8 opeq1 4802 . . . . . . 7 (𝑦 = 𝑥 → ⟨𝑦, (𝐹𝑥)⟩ = ⟨𝑥, (𝐹𝑥)⟩)
98eleq1d 2897 . . . . . 6 (𝑦 = 𝑥 → (⟨𝑦, (𝐹𝑥)⟩ ∈ 𝐹 ↔ ⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹))
107, 9spcev 3606 . . . . 5 (⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹 → ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
116, 10syl 17 . . . 4 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
12 fvex 6682 . . . . 5 (𝐹𝑥) ∈ V
1312elrn2 5820 . . . 4 ((𝐹𝑥) ∈ ran 𝐹 ↔ ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
1411, 13sylibr 236 . . 3 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹)
155, 14vtoclg 3567 . 2 (𝐴 ∈ dom 𝐹 → ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹))
1615anabsi7 669 1 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110  ⟨cop 4572  dom cdm 5554  ran crn 5555  Fun wfun 6348  ‘cfv 6354 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6313  df-fun 6356  df-fn 6357  df-fv 6362 This theorem is referenced by:  nelrnfvne  6844  fnfvelrn  6847  eldmrexrn  6856  fvn0fvelrn  6924  funfvima  6991  elunirn  7009  rankwflemb  9221  dfac9  9561  fin1a2lem6  9826  gsumpropd2lem  17888  iedgedg  26834  usgredg3  26997  ushgredgedg  27010  ushgredgedgloop  27012  subgruhgredgd  27065  edginwlk  27415  iedginwlk  27417  opfv  30392  fnpreimac  30415  ccatf1  30625  swrdrn2  30628  funeldmb  33006  nofv  33164  sltres  33169  nolt02olem  33198  nosupno  33203  bj-elccinfty  34495  bj-minftyccb  34506  icoreunrn  34639  indexdom  35008  diaclN  38185  dia1elN  38189  docaclN  38259  dibclN  38297  dfac21  39664  harval3  39902  gneispace  40482  cncmpmax  41287  icccncfext  42168  stoweidlem27  42311  stoweidlem29  42313  stoweidlem59  42343  fourierdlem20  42411  fourierdlem63  42453  fourierdlem76  42466  fourierdlem82  42472  fourierdlem93  42483  fourierdlem113  42503  fge0iccico  42651  sge0sn  42660  sge0tsms  42661  sge0cl  42662  sge0isum  42708  hoicvr  42829  funressndmfvrn  43278  afvelrn  43366  isomushgr  43990  ushrisomgr  44005  suppdm  44564
 Copyright terms: Public domain W3C validator