Theorem ffvelrnda 5601

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 5599	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	sylan 281	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2128  ⟶wf 5165  ‘cfv 5169

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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-id 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-fv 5177

This theorem is referenced by:  ffvelrnd  5602  f1ocnvdm  5728  foeqcnvco  5737  f1oiso2  5774  offeq  6042  suppssof1  6046  ofco  6047  caofref  6050  caofinvl  6051  caofcom  6052  caofrss  6053  caoftrn  6054  smofvon2dm  6240  smofvon  6243  mapxpen  6790  xpmapenlem  6791  en2eqpr  6849  supisoex  6949  ordiso2  6973  omp1eomlem  7032  ctssdccl  7049  ctssdc  7051  enumctlemm  7052  enomnilem  7075  fodjuomnilemdc  7081  ismkvnex  7092  enmkvlem  7098  enwomnilem  7106  cc3  7182  cauappcvgprlemladdru  7570  cauappcvgprlemladdrl  7571  caucvgprlemladdrl  7592  caucvgprprlemopu  7613  caucvgprprlemexbt  7620  caucvgprprlemexb  7621  caucvgsrlemcl  7703  caucvgsrlemfv  7705  caucvgsrlemcau  7707  caucvgsrlembound  7708  caucvgsrlemoffval  7710  caucvgsrlemofff  7711  caucvgsrlemoffgt1  7713  caucvgsrlemoffres  7714  caucvgsr  7716  axcaucvglemcl  7809  frecuzrdgfunlem  10311  monoord2  10369  seq3f1o  10396  seq3homo  10402  seqfeq3  10404  zfz1isolemiso  10703  seq3coll  10706  resqrexlemfp1  10902  resqrexlemover  10903  resqrexlemdec  10904  resqrexlemlo  10906  resqrexlemcalc1  10907  resqrexlemcalc2  10908  resqrexlemcalc3  10909  resqrexlemgt0  10913  resqrexlemsqa  10917  clim2ser  11227  clim2ser2  11228  isermulc2  11230  iserle  11232  climserle  11235  climrecvg1n  11238  climcvg1nlem  11239  summodclem3  11270  summodclem2a  11271  fsumgcl  11276  fsum3  11277  fsumf1o  11280  isumss  11281  fisumss  11282  fsumcl2lem  11288  fsumadd  11296  isumclim3  11313  isummulc2  11316  isumrecl  11319  isumadd  11321  fsummulc2  11338  iserabs  11365  cvgcmpub  11366  isumshft  11380  isumsplit  11381  mertensabs  11427  clim2prod  11429  clim2divap  11430  prodfap0  11435  prodfdivap  11437  prodmodclem3  11465  prodmodclem2a  11466  fprodseq  11473  fprodf1o  11478  prodssdc  11479  fprodssdc  11480  fprodmul  11481  efcj  11563  nn0seqcvgd  11909  algrp1  11914  alginv  11915  algcvg  11916  algcvga  11919  algfx  11920  eucalgcvga  11926  eulerthlem1  12090  eulerthlemh  12094  eulerthlemth  12095  cnptoprest2  12611  lmss  12617  txcnmpt  12644  txlm  12650  lmcn2  12651  psmetxrge0  12703  metcnp  12883  climcncf  12942  negfcncf  12960  ivthdec  12993  dvcnp2cntop  13034  dvaddxxbr  13036  dvimulf  13041  dvcj  13044  dvfre  13045  nninfall  13552  nninffeq  13563  refeq  13570  trilpolemclim  13578  trilpolemcl  13579  trilpolemisumle  13580  trilpolemeq1  13582  iswomni0  13593