Theorem ffvelrnda 5631

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypothesis

Ref	Expression
ffvelrnd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffvelrnda	⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelrnda

Step	Hyp	Ref	Expression
1		ffvelrnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffvelrn 5629	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	sylan 281	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ⟶wf 5194  ‘cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-sbc 2956  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206

This theorem is referenced by:  ffvelrnd  5632  f1ocnvdm  5760  foeqcnvco  5769  f1oiso2  5806  offeq  6074  suppssof1  6078  ofco  6079  caofref  6082  caofinvl  6083  caofcom  6084  caofrss  6085  caoftrn  6086  smofvon2dm  6275  smofvon  6278  mapxpen  6826  xpmapenlem  6827  en2eqpr  6885  supisoex  6986  ordiso2  7012  omp1eomlem  7071  ctssdccl  7088  ctssdc  7090  enumctlemm  7091  enomnilem  7114  fodjuomnilemdc  7120  ismkvnex  7131  enmkvlem  7137  enwomnilem  7145  nninfwlporlemd  7148  nninfwlporlem  7149  nninfwlpoimlemginf  7152  cc3  7230  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgprprlemopu  7661  caucvgprprlemexbt  7668  caucvgprprlemexb  7669  caucvgsrlemcl  7751  caucvgsrlemfv  7753  caucvgsrlemcau  7755  caucvgsrlembound  7756  caucvgsrlemoffval  7758  caucvgsrlemofff  7759  caucvgsrlemoffgt1  7761  caucvgsrlemoffres  7762  caucvgsr  7764  axcaucvglemcl  7857  frecuzrdgfunlem  10375  monoord2  10433  seq3f1o  10460  seq3homo  10466  seqfeq3  10468  zfz1isolemiso  10774  seq3coll  10777  resqrexlemfp1  10973  resqrexlemover  10974  resqrexlemdec  10975  resqrexlemlo  10977  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrexlemcalc3  10980  resqrexlemgt0  10984  resqrexlemsqa  10988  clim2ser  11300  clim2ser2  11301  isermulc2  11303  iserle  11305  climserle  11308  climrecvg1n  11311  climcvg1nlem  11312  summodclem3  11343  summodclem2a  11344  fsumgcl  11349  fsum3  11350  fsumf1o  11353  isumss  11354  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  isumclim3  11386  isummulc2  11389  isumrecl  11392  isumadd  11394  fsummulc2  11411  iserabs  11438  cvgcmpub  11439  isumshft  11453  isumsplit  11454  mertensabs  11500  clim2prod  11502  clim2divap  11503  prodfap0  11508  prodfdivap  11510  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  efcj  11636  nn0seqcvgd  11995  algrp1  12000  alginv  12001  algcvg  12002  algcvga  12005  algfx  12006  eucalgcvga  12012  eulerthlem1  12181  eulerthlemh  12185  eulerthlemth  12186  pcmptcl  12294  pcmpt  12295  1arithlem4  12318  nninfdclemf1  12407  grpinvcl  12751  cnptoprest2  13034  lmss  13040  txcnmpt  13067  txlm  13073  lmcn2  13074  psmetxrge0  13126  metcnp  13306  climcncf  13365  negfcncf  13383  ivthdec  13416  dvcnp2cntop  13457  dvaddxxbr  13459  dvimulf  13464  dvcj  13467  dvfre  13468  lgscllem  13702  lgsfle1  13704  lgsval4a  13717  lgsneg  13719  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  nninfall  14042  nninffeq  14053  refeq  14060  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  iswomni0  14083