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

Theorem fvelrn 7091
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 2817 . . . . 5 (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹𝐴 ∈ dom 𝐹))
21anbi2d 628 . . . 4 (𝑥 = 𝐴 → ((Fun 𝐹𝑥 ∈ dom 𝐹) ↔ (Fun 𝐹𝐴 ∈ dom 𝐹)))
3 fveq2 6902 . . . . 5 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
43eleq1d 2814 . . . 4 (𝑥 = 𝐴 → ((𝐹𝑥) ∈ ran 𝐹 ↔ (𝐹𝐴) ∈ ran 𝐹))
52, 4imbi12d 343 . . 3 (𝑥 = 𝐴 → (((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹) ↔ ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)))
6 funfvop 7064 . . . . 5 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹)
7 vex 3477 . . . . . 6 𝑥 ∈ V
8 opeq1 4878 . . . . . . 7 (𝑦 = 𝑥 → ⟨𝑦, (𝐹𝑥)⟩ = ⟨𝑥, (𝐹𝑥)⟩)
98eleq1d 2814 . . . . . 6 (𝑦 = 𝑥 → (⟨𝑦, (𝐹𝑥)⟩ ∈ 𝐹 ↔ ⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹))
107, 9spcev 3595 . . . . 5 (⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹 → ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
116, 10syl 17 . . . 4 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
12 fvex 6915 . . . . 5 (𝐹𝑥) ∈ V
1312elrn2 5899 . . . 4 ((𝐹𝑥) ∈ ran 𝐹 ↔ ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
1411, 13sylibr 233 . . 3 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹)
155, 14vtoclg 3542 . 2 (𝐴 ∈ dom 𝐹 → ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹))
1615anabsi7 669 1 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wex 1773  wcel 2098  cop 4638  dom cdm 5682  ran crn 5683  Fun wfun 6547  cfv 6553
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-iota 6505  df-fun 6555  df-fn 6556  df-fv 6561
This theorem is referenced by:  nelrnfvne  7092  fnfvelrn  7095  eldmrexrn  7106  fvn0fvelrnOLD  7178  funfvima  7248  elunirn  7267  funeldmb  7373  rankwflemb  9824  dfac9  10167  fin1a2lem6  10436  gsumpropd2lem  18646  nofv  27610  sltres  27615  nolt02olem  27647  nosupno  27656  noinfno  27671  iedgedg  28883  usgredg3  29049  ushgredgedg  29062  ushgredgedgloop  29064  subgruhgredgd  29117  edginwlk  29469  iedginwlk  29471  opfv  32452  fnpreimac  32478  ccatf1  32693  swrdrn2  32696  zartopn  33509  zarmxt1  33514  bj-elccinfty  36726  bj-minftyccb  36737  icoreunrn  36871  indexdom  37240  diaclN  40555  dia1elN  40559  docaclN  40629  dibclN  40667  sticksstones1  41650  dfac21  42521  harval3  42999  gneispace  43595  cncmpmax  44425  icccncfext  45304  stoweidlem27  45444  stoweidlem29  45446  stoweidlem59  45476  fourierdlem20  45544  fourierdlem63  45586  fourierdlem76  45599  fourierdlem82  45605  fourierdlem93  45616  fourierdlem113  45636  fge0iccico  45787  sge0sn  45796  sge0tsms  45797  sge0cl  45798  sge0isum  45844  hoicvr  45965  funressndmfvrn  46455  fcores  46478  afvelrn  46577  gricushgr  47261  ushggricedg  47271  suppdm  47656
  Copyright terms: Public domain W3C validator