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.

Step	Hyp	Ref	Expression
1		eleq1 2893	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝐴 ∈ dom 𝐹))
2	1	anbi2d 624	. . . 4 ⊢ (𝑥 = 𝐴 → ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) ↔ (Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹)))
3		fveq2 6432	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
4	3	eleq1d 2890	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) ∈ ran 𝐹 ↔ (𝐹‘𝐴) ∈ ran 𝐹))
5	2, 4	imbi12d 336	. . 3 ⊢ (𝑥 = 𝐴 → (((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) ↔ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)))
6		funfvop 6577	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ⟨𝑥, (𝐹‘𝑥)⟩ ∈ 𝐹)
7		vex 3416	. . . . . 6 ⊢ 𝑥 ∈ V
8		opeq1 4622	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ⟨𝑦, (𝐹‘𝑥)⟩ = ⟨𝑥, (𝐹‘𝑥)⟩)
9	8	eleq1d 2890	. . . . . 6 ⊢ (𝑦 = 𝑥 → (⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹 ↔ ⟨𝑥, (𝐹‘𝑥)⟩ ∈ 𝐹))
10	7, 9	spcev 3516	. . . . 5 ⊢ (⟨𝑥, (𝐹‘𝑥)⟩ ∈ 𝐹 → ∃𝑦⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹)
11	6, 10	syl 17	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ∃𝑦⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹)
12		fvex 6445	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
13	12	elrn2 5597	. . . 4 ⊢ ((𝐹‘𝑥) ∈ ran 𝐹 ↔ ∃𝑦⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹)
14	11, 13	sylibr 226	. . 3 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹)
15	5, 14	vtoclg 3481	. 2 ⊢ (𝐴 ∈ dom 𝐹 → ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹))
16	15	anabsi7 663	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)

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