Theorem fvelrn 7066

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 2822	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝐴 ∈ dom 𝐹))
2	1	anbi2d 630	. . . 4 ⊢ (𝑥 = 𝐴 → ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) ↔ (Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹)))
3		fveq2 6876	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
4	3	eleq1d 2819	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) ∈ ran 𝐹 ↔ (𝐹‘𝐴) ∈ ran 𝐹))
5	2, 4	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → (((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) ↔ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)))
6		funfvop 7040	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ⟨𝑥, (𝐹‘𝑥)⟩ ∈ 𝐹)
7		vex 3463	. . . . . 6 ⊢ 𝑥 ∈ V
8		opeq1 4849	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ⟨𝑦, (𝐹‘𝑥)⟩ = ⟨𝑥, (𝐹‘𝑥)⟩)
9	8	eleq1d 2819	. . . . . 6 ⊢ (𝑦 = 𝑥 → (⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹 ↔ ⟨𝑥, (𝐹‘𝑥)⟩ ∈ 𝐹))
10	7, 9	spcev 3585	. . . . 5 ⊢ (⟨𝑥, (𝐹‘𝑥)⟩ ∈ 𝐹 → ∃𝑦⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹)
11	6, 10	syl 17	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ∃𝑦⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹)
12		fvex 6889	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
13	12	elrn2 5872	. . . 4 ⊢ ((𝐹‘𝑥) ∈ ran 𝐹 ↔ ∃𝑦⟨𝑦, (𝐹‘𝑥)⟩ ∈ 𝐹)
14	11, 13	sylibr 234	. . 3 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹)
15	5, 14	vtoclg 3533	. 2 ⊢ (𝐴 ∈ dom 𝐹 → ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹))
16	15	anabsi7 671	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ⟨cop 4607  dom cdm 5654  ran crn 5655  Fun wfun 6525  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is referenced by:  nelrnfvne  7067  fnfvelrn  7070  eldmrexrn  7081  fvn0fvelrnOLD  7153  funfvima  7222  elunirn  7243  funeldmb  7352  rankwflemb  9807  dfac9  10151  fin1a2lem6  10419  gsumpropd2lem  18657  nofv  27621  sltres  27626  nolt02olem  27658  nosupno  27667  noinfno  27682  iedgedg  29029  usgredg3  29195  ushgredgedg  29208  ushgredgedgloop  29210  subgruhgredgd  29263  edginwlk  29615  iedginwlk  29617  cyclnumvtx  29782  opfv  32622  fnpreimac  32649  ccatf1  32924  swrdrn2  32930  zartopn  33906  zarmxt1  33911  bj-elccinfty  37232  bj-minftyccb  37243  icoreunrn  37377  indexdom  37758  diaclN  41069  dia1elN  41073  docaclN  41143  dibclN  41181  sticksstones1  42159  dfac21  43090  harval3  43562  gneispace  44158  cncmpmax  45056  icccncfext  45916  stoweidlem27  46056  stoweidlem29  46058  stoweidlem59  46088  fourierdlem20  46156  fourierdlem63  46198  fourierdlem76  46211  fourierdlem82  46217  fourierdlem93  46228  fourierdlem113  46248  fge0iccico  46399  sge0sn  46408  sge0tsms  46409  sge0cl  46410  sge0isum  46456  hoicvr  46577  funressndmfvrn  47073  fcores  47096  afvelrn  47197  isubgredg  47879  gricushgr  47930  ushggricedg  47940  suppdm  48486