Theorem fnfvelrn 3889

Description: A function's value belongs to its range.

Assertion

Ref	Expression
fnfvelrn	|- ((F Fn A /\ B e. A) -> (F` B) e. ran F)

Proof of Theorem fnfvelrn

Step	Hyp	Ref	Expression
1		fvelrn 3888	. 2 |- ((Fun F /\ B e. dom F) -> (F` B) e. ran F)
2	1	funfni 3663	1 |- ((F Fn A /\ B e. A) -> (F` B) e. ran F)

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 990  ran crn 3226   Fn wfn 3232  ` cfv 3237

This theorem is referenced by:  ffvelrn 3890  rnssopab 3901  fopabcos 3909  fnoprvalrn 4116  fo1stres 4173  fo2ndres 4174  phplem4 4600  inf0 4692  noinfep 4726  aceq5 4826  cardinfima 4980  alephfplem1 4985  alephfplem3 4987  alephfp 4989  fseqsupubi 6586  om2uzrani 6592  seqzcl 6681  seq1ublem 7034  seq1ubi 7035  climsupi 7278  ruclem33 7667  ruclem35 7669  ghgrpilem1 8252  ghgrpilem3 8254  ghgrpilem4 8255  pjoi0 9782  pjssdif1i 10220  pjadj3 10233  pjcmmul1i 10247  pjcmmul2i 10248  pj3si 10253

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-fv 3253

Copyright terms: Public domain