Theorem fnfvelrn 7112

Description: A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)

Assertion

Ref	Expression
fnfvelrn	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)

Proof of Theorem fnfvelrn

Step	Hyp	Ref	Expression
1		fvelrn 7108	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ ran 𝐹)
2	1	funfni 6675	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ran crn 5659   Fn wfn 6561  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574

This theorem is used by:  ffvelcdm  7113  fnfvelrnd  7114  fvcofneq  7125  fnovrn  7628  offvalfv  7747  fo1stres  8061  fo2ndres  8062  offsplitfpar  8167  fo2ndf  8169  seqomlem3  8500  seqomlem4  8501  phplem2  9258  indexfi  9387  dffi3  9460  ordtypelem7  9555  inf0  9659  infdifsn  9695  noinfep  9698  cantnflem3  9729  cantnf  9731  cardinfima  10215  alephfplem1  10222  alephfplem3  10224  alephfp  10226  dfac5  10246  dfac12lem2  10262  cfflb  10376  sornom  10394  fin23lem16  10452  fin23lem20  10454  isf32lem2  10471  axcc2lem  10553  axdc3lem2  10568  ttukeylem6  10631  konigthlem  10692  pwcfsdom  10707  pwfseqlem1  10782  gch2  10799  1nn  12386  peano2nn  12387  rpnnen1lem5  13149  om2uzrani  14135  uzrdglem  14140  uzrdg0i  14142  fseqsupubi  14161  ccatrn  14776  sgnrn  15294  uzin2  15556  climsup  15881  ruclem12  16453  0ram  17242  setcepi  18313  acsmapd  18778  cycsubgcl  19471  ghmrn  19493  conjnmz  19516  pmtrrn  19722  sylow1lem4  19866  pgpssslw  19879  sylow2blem3  19887  sylow3lem2  19893  efgsfo  20004  gexex  20118  gsumval3eu  20169  gsumzsplit  20192  pjfo  22076  issubassa2  22255  mplbas2  22406  mpfconst  22473  mpfproj  22474  mpfind  22479  pf1const  22719  pf1id  22720  mpfpf1  22724  pf1mpf  22725  toprntopon  23298  cmpsub  23773  conncn  23799  2ndcctbss  23829  2ndcdisj  23830  2ndcsep  23833  iskgen2  23922  kgen2cn  23933  ptbasfi  23955  ptcnplem  23995  isr0  24111  r0cld  24112  zfbas  24270  uzrest  24271  rnelfm  24327  tmdgsum2  24470  evth  25335  bcth3  25707  ivthicc  25834  ovolmge0  25853  ovollb2lem  25864  ovolunlem1a  25872  ovoliunlem1  25878  ovoliun  25881  ovolicc2lem4  25896  voliunlem1  25926  voliunlem3  25928  volsup  25932  ioombl1lem2  25935  ioombl1lem4  25937  uniioombllem2  25959  uniioombllem3  25961  vitalilem2  25985  vitalilem4  25987  mbflimsup  26042  itg11  26067  i1faddlem  26069  i1fmullem  26070  itg1mulc  26080  i1fres  26081  itg1climres  26090  mbfi1fseqlem3  26093  itg2seq  26118  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  itg2cnlem1  26137  limciun  26269  dvcnvlem  26351  dvivthlem2  26384  dvivth  26385  lhop1lem  26388  lhop1  26389  lhop2  26390  aalioulem3  26718  basellem3  27467  nodenselem8  28105  noseq0  28733  noseqp1  28734  noseqrdg0  28750  tgelrnln  29155  wlkiswwlks1  30513  ubthlem1  31529  pjrni  32361  pjoi0  32376  hmopidmchi  32810  hmopidmpji  32811  pjssdif1i  32834  dfpjop  32841  pjadj3  32847  elpjrn  32849  pjcmul1i  32860  pjcmul2i  32861  pj3si  32866  ofrn2  33332  prodindf  33525  mgcf1o  33663  cycpmfvlem  33772  cycpmfv1  33773  cycpmfv2  33774  locfinreflem  34583  cnre2csqlem  34653  elmrsubrn  36493  elmsubrn  36501  msubrn  36502  elmsta  36521  vhmcls  36539  mclsppslem  36556  neibastop2lem  37363  tailfb  37380  fvineqsneu  38602  ptrecube  38806  heicant  38841  mblfinlem2  38844  ftc1anclem7  38885  ftc1anc  38887  sstotbnd2  38974  prdsbnd  38993  heibor1lem  39009  heiborlem1  39011  dihcl  42593  dih0rn  42607  dih1dimatlem  42652  dihlspsnssN  42655  dochocss  42689  hdmaprnlem17N  43186  hgmaprnlem1N  43219  nacsfix  43989  kercvrlsm  44351  pwssplit4  44357  tfsconcatrev  44611  orbitinit  46210  orbitcl  46211  climinf  46891  climinf2lem  46989  limsupvaluz2  47021  supcnvlimsup  47023  fourierdlem25  47415  fourierdlem42  47432  fourierdlem54  47443  fourierdlem64  47453  fourierdlem65  47454  sge0le  47690  sge0seq  47729  imaelsetpreimafv  48750