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

Theorem fvelrn 6600
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 2893 . . . . 5 (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹𝐴 ∈ dom 𝐹))
21anbi2d 624 . . . 4 (𝑥 = 𝐴 → ((Fun 𝐹𝑥 ∈ dom 𝐹) ↔ (Fun 𝐹𝐴 ∈ dom 𝐹)))
3 fveq2 6432 . . . . 5 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
43eleq1d 2890 . . . 4 (𝑥 = 𝐴 → ((𝐹𝑥) ∈ ran 𝐹 ↔ (𝐹𝐴) ∈ ran 𝐹))
52, 4imbi12d 336 . . 3 (𝑥 = 𝐴 → (((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹) ↔ ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)))
6 funfvop 6577 . . . . 5 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹)
7 vex 3416 . . . . . 6 𝑥 ∈ V
8 opeq1 4622 . . . . . . 7 (𝑦 = 𝑥 → ⟨𝑦, (𝐹𝑥)⟩ = ⟨𝑥, (𝐹𝑥)⟩)
98eleq1d 2890 . . . . . 6 (𝑦 = 𝑥 → (⟨𝑦, (𝐹𝑥)⟩ ∈ 𝐹 ↔ ⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹))
107, 9spcev 3516 . . . . 5 (⟨𝑥, (𝐹𝑥)⟩ ∈ 𝐹 → ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
116, 10syl 17 . . . 4 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
12 fvex 6445 . . . . 5 (𝐹𝑥) ∈ V
1312elrn2 5597 . . . 4 ((𝐹𝑥) ∈ ran 𝐹 ↔ ∃𝑦𝑦, (𝐹𝑥)⟩ ∈ 𝐹)
1411, 13sylibr 226 . . 3 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹)
155, 14vtoclg 3481 . 2 (𝐴 ∈ dom 𝐹 → ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹))
1615anabsi7 663 1 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐹𝐴) ∈ ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wex 1880  wcel 2166  cop 4402  dom cdm 5341  ran crn 5342  Fun wfun 6116  cfv 6122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pr 5126
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ral 3121  df-rex 3122  df-rab 3125  df-v 3415  df-sbc 3662  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-uni 4658  df-br 4873  df-opab 4935  df-id 5249  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-iota 6085  df-fun 6124  df-fn 6125  df-fv 6130
This theorem is referenced by:  nelrnfvne  6601  fnfvelrn  6604  eldmrexrn  6613  fvn0fvelrn  6680  funfvima  6747  elunirn  6763  rankwflemb  8932  dfac9  9272  fin1a2lem6  9541  gsumpropd2lem  17625  iedgedg  26347  usgredg3  26511  ushgredgedg  26524  ushgredgedgloop  26526  ushgredgedgloopOLD  26527  subgruhgredgd  26580  edginwlk  26931  iedginwlk  26933  opfv  29996  funeldmb  32202  nofv  32348  sltres  32353  nolt02olem  32382  nosupno  32387  bj-elccinfty  33640  bj-minftyccb  33651  icoreunrn  33751  indexdom  34071  diaclN  37124  dia1elN  37128  docaclN  37198  dibclN  37236  dfac21  38478  gneispace  39271  cncmpmax  40008  icccncfext  40894  stoweidlem27  41037  stoweidlem29  41039  stoweidlem59  41069  fourierdlem20  41137  fourierdlem63  41179  fourierdlem76  41192  fourierdlem82  41198  fourierdlem93  41209  fourierdlem113  41229  fge0iccico  41377  sge0sn  41386  sge0tsms  41387  sge0cl  41388  sge0isum  41434  hoicvr  41555  funressndmfvrn  41974  afvelrn  42069  isomushgr  42543  ushrisomgr  42558  suppdm  43146
  Copyright terms: Public domain W3C validator