Theorem ffvelcdmda 5782

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

Hypothesis

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

Assertion

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

Proof of Theorem ffvelcdmda

Step	Hyp	Ref	Expression
1		ffvelcdmd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffvelcdm 5780	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	sylan 283	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ⟶wf 5322  ‘cfv 5326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  ffvelcdmd  5783  f1ocnvdm  5922  foeqcnvco  5931  f1oiso2  5968  offeq  6249  suppssof1  6253  ofco  6254  caofref  6260  caofinvl  6261  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  caofcom  6266  caofrss  6267  caoftrn  6268  caofdig  6269  smofvon2dm  6462  smofvon  6465  pw2f1odclem  7020  mapxpen  7034  xpmapenlem  7035  en2eqpr  7099  supisoex  7208  ordiso2  7234  omp1eomlem  7293  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  enomnilem  7337  fodjuomnilemdc  7343  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemginf  7375  cc3  7487  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlemcau  8013  caucvgsrlembound  8014  caucvgsrlemoffval  8016  caucvgsrlemofff  8017  caucvgsrlemoffgt1  8019  caucvgsrlemoffres  8020  caucvgsr  8022  axcaucvglemcl  8115  ofnegsub  9142  frecuzrdgfunlem  10682  monoord2  10749  seq3f1o  10780  seqf1oglem2  10783  seqf1og  10784  seq3homo  10790  seqfeq3  10792  zfz1isolemiso  11104  seq3coll  11107  wrdsymbcl  11131  ccatcl  11174  resqrexlemfp1  11574  resqrexlemover  11575  resqrexlemdec  11576  resqrexlemlo  11578  resqrexlemcalc1  11579  resqrexlemcalc2  11580  resqrexlemcalc3  11581  resqrexlemgt0  11585  resqrexlemsqa  11589  clim2ser  11902  clim2ser2  11903  isermulc2  11905  iserle  11907  climserle  11910  climrecvg1n  11913  climcvg1nlem  11914  summodclem3  11946  summodclem2a  11947  fsumgcl  11952  fsum3  11953  fsumf1o  11956  isumss  11957  fisumss  11958  fsumcl2lem  11964  fsumadd  11972  isumclim3  11989  isummulc2  11992  isumrecl  11995  isumadd  11997  fsummulc2  12014  iserabs  12041  cvgcmpub  12042  isumshft  12056  isumsplit  12057  mertensabs  12103  clim2prod  12105  clim2divap  12106  prodfap0  12111  prodfdivap  12113  prodmodclem3  12141  prodmodclem2a  12142  fprodseq  12149  fprodf1o  12154  prodssdc  12155  fprodssdc  12156  fprodmul  12157  efcj  12239  nninfctlemfo  12616  nn0seqcvgd  12618  algrp1  12623  alginv  12624  algcvg  12625  algcvga  12628  algfx  12629  eucalgcvga  12635  eulerthlem1  12804  eulerthlemh  12808  eulerthlemth  12809  pcmptcl  12920  pcmpt  12921  1arithlem4  12944  nninfdclemf1  13078  prdsplusgsgrpcl  13502  prdssgrpd  13503  prdsplusgcl  13534  prdsidlem  13535  prdsmndd  13536  gsumwsubmcl  13584  gsumwmhm  13586  grpinvcl  13636  prdsinvlem  13696  pwsinvg  13700  pwssub  13701  mhmmulg  13755  ghminv  13842  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  rhmdvdsr  14195  psrlinv  14704  psr1clfi  14708  mplsubgfilemcl  14719  cnptoprest2  14970  lmss  14976  txcnmpt  15003  txlm  15009  lmcn2  15010  psmetxrge0  15062  metcnp  15242  climcncf  15314  negfcncf  15336  ivthdec  15374  ivthreinc  15375  dvcnp2cntop  15429  dvaddxxbr  15431  dvimulf  15436  dvcj  15439  dvfre  15440  elply2  15465  plyaddlem1  15477  plymullem1  15478  plycolemc  15488  plyco  15489  dvply2g  15496  lgscllem  15742  lgsfle1  15744  lgsval4a  15757  lgsneg  15759  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  uhgrss  15932  uhgrm  15935  upgrss  15956  upgrm  15957  upgr1or2  15958  umgredg2en  15966  lfgredg2dom  15989  usgrss  16034  depindlem1  16351  depindlem2  16352  pw1map  16622  nninfall  16637  nninffeq  16648  refeq  16658  trilpolemclim  16666  trilpolemcl  16667  trilpolemisumle  16668  trilpolemeq1  16670  iswomni0  16682