Theorem ffvelcdmda 5668

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160  ⟶wf 5228  ‘cfv 5232

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-fv 5240

This theorem is referenced by:  ffvelcdmd  5669  f1ocnvdm  5799  foeqcnvco  5808  f1oiso2  5845  offeq  6115  suppssof1  6119  ofco  6120  caofref  6123  caofinvl  6124  caofcom  6125  caofrss  6126  caoftrn  6127  smofvon2dm  6316  smofvon  6319  pw2f1odclem  6857  mapxpen  6871  xpmapenlem  6872  en2eqpr  6930  supisoex  7033  ordiso2  7059  omp1eomlem  7118  ctssdccl  7135  ctssdc  7137  enumctlemm  7138  enomnilem  7161  fodjuomnilemdc  7167  ismkvnex  7178  enmkvlem  7184  enwomnilem  7192  nninfwlporlemd  7195  nninfwlporlem  7196  nninfwlpoimlemginf  7199  cc3  7292  cauappcvgprlemladdru  7680  cauappcvgprlemladdrl  7681  caucvgprlemladdrl  7702  caucvgprprlemopu  7723  caucvgprprlemexbt  7730  caucvgprprlemexb  7731  caucvgsrlemcl  7813  caucvgsrlemfv  7815  caucvgsrlemcau  7817  caucvgsrlembound  7818  caucvgsrlemoffval  7820  caucvgsrlemofff  7821  caucvgsrlemoffgt1  7823  caucvgsrlemoffres  7824  caucvgsr  7826  axcaucvglemcl  7919  frecuzrdgfunlem  10445  monoord2  10503  seq3f1o  10530  seq3homo  10536  seqfeq3  10538  zfz1isolemiso  10846  seq3coll  10849  resqrexlemfp1  11045  resqrexlemover  11046  resqrexlemdec  11047  resqrexlemlo  11049  resqrexlemcalc1  11050  resqrexlemcalc2  11051  resqrexlemcalc3  11052  resqrexlemgt0  11056  resqrexlemsqa  11060  clim2ser  11372  clim2ser2  11373  isermulc2  11375  iserle  11377  climserle  11380  climrecvg1n  11383  climcvg1nlem  11384  summodclem3  11415  summodclem2a  11416  fsumgcl  11421  fsum3  11422  fsumf1o  11425  isumss  11426  fisumss  11427  fsumcl2lem  11433  fsumadd  11441  isumclim3  11458  isummulc2  11461  isumrecl  11464  isumadd  11466  fsummulc2  11483  iserabs  11510  cvgcmpub  11511  isumshft  11525  isumsplit  11526  mertensabs  11572  clim2prod  11574  clim2divap  11575  prodfap0  11580  prodfdivap  11582  prodmodclem3  11610  prodmodclem2a  11611  fprodseq  11618  fprodf1o  11623  prodssdc  11624  fprodssdc  11625  fprodmul  11626  efcj  11708  nn0seqcvgd  12068  algrp1  12073  alginv  12074  algcvg  12075  algcvga  12078  algfx  12079  eucalgcvga  12085  eulerthlem1  12254  eulerthlemh  12258  eulerthlemth  12259  pcmptcl  12369  pcmpt  12370  1arithlem4  12393  nninfdclemf1  12498  grpinvcl  12985  mhmmulg  13096  ghminv  13182  rhmdvdsr  13518  cnptoprest2  14177  lmss  14183  txcnmpt  14210  txlm  14216  lmcn2  14217  psmetxrge0  14269  metcnp  14449  climcncf  14508  negfcncf  14526  ivthdec  14559  dvcnp2cntop  14600  dvaddxxbr  14602  dvimulf  14607  dvcj  14610  dvfre  14611  lgscllem  14846  lgsfle1  14848  lgsval4a  14861  lgsneg  14863  lgsdir  14874  lgsdilem2  14875  lgsdi  14876  lgsne0  14877  nninfall  15197  nninffeq  15208  refeq  15215  trilpolemclim  15223  trilpolemcl  15224  trilpolemisumle  15225  trilpolemeq1  15227  iswomni0  15238