ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ffvelcdmda GIF version

Theorem ffvelcdmda 5646
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
StepHypRef Expression
1 ffvelcdmd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffvelcdm 5644 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
31, 2sylan 283 1 ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wf 5207  cfv 5211
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-id 4289  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-iota 5173  df-fun 5213  df-fn 5214  df-f 5215  df-fv 5219
This theorem is referenced by:  ffvelcdmd  5647  f1ocnvdm  5775  foeqcnvco  5784  f1oiso2  5821  offeq  6089  suppssof1  6093  ofco  6094  caofref  6097  caofinvl  6098  caofcom  6099  caofrss  6100  caoftrn  6101  smofvon2dm  6290  smofvon  6293  mapxpen  6841  xpmapenlem  6842  en2eqpr  6900  supisoex  7001  ordiso2  7027  omp1eomlem  7086  ctssdccl  7103  ctssdc  7105  enumctlemm  7106  enomnilem  7129  fodjuomnilemdc  7135  ismkvnex  7146  enmkvlem  7152  enwomnilem  7160  nninfwlporlemd  7163  nninfwlporlem  7164  nninfwlpoimlemginf  7167  cc3  7245  cauappcvgprlemladdru  7633  cauappcvgprlemladdrl  7634  caucvgprlemladdrl  7655  caucvgprprlemopu  7676  caucvgprprlemexbt  7683  caucvgprprlemexb  7684  caucvgsrlemcl  7766  caucvgsrlemfv  7768  caucvgsrlemcau  7770  caucvgsrlembound  7771  caucvgsrlemoffval  7773  caucvgsrlemofff  7774  caucvgsrlemoffgt1  7776  caucvgsrlemoffres  7777  caucvgsr  7779  axcaucvglemcl  7872  frecuzrdgfunlem  10392  monoord2  10450  seq3f1o  10477  seq3homo  10483  seqfeq3  10485  zfz1isolemiso  10790  seq3coll  10793  resqrexlemfp1  10989  resqrexlemover  10990  resqrexlemdec  10991  resqrexlemlo  10993  resqrexlemcalc1  10994  resqrexlemcalc2  10995  resqrexlemcalc3  10996  resqrexlemgt0  11000  resqrexlemsqa  11004  clim2ser  11316  clim2ser2  11317  isermulc2  11319  iserle  11321  climserle  11324  climrecvg1n  11327  climcvg1nlem  11328  summodclem3  11359  summodclem2a  11360  fsumgcl  11365  fsum3  11366  fsumf1o  11369  isumss  11370  fisumss  11371  fsumcl2lem  11377  fsumadd  11385  isumclim3  11402  isummulc2  11405  isumrecl  11408  isumadd  11410  fsummulc2  11427  iserabs  11454  cvgcmpub  11455  isumshft  11469  isumsplit  11470  mertensabs  11516  clim2prod  11518  clim2divap  11519  prodfap0  11524  prodfdivap  11526  prodmodclem3  11554  prodmodclem2a  11555  fprodseq  11562  fprodf1o  11567  prodssdc  11568  fprodssdc  11569  fprodmul  11570  efcj  11652  nn0seqcvgd  12011  algrp1  12016  alginv  12017  algcvg  12018  algcvga  12021  algfx  12022  eucalgcvga  12028  eulerthlem1  12197  eulerthlemh  12201  eulerthlemth  12202  pcmptcl  12310  pcmpt  12311  1arithlem4  12334  nninfdclemf1  12423  grpinvcl  12798  mhmmulg  12899  cnptoprest2  13373  lmss  13379  txcnmpt  13406  txlm  13412  lmcn2  13413  psmetxrge0  13465  metcnp  13645  climcncf  13704  negfcncf  13722  ivthdec  13755  dvcnp2cntop  13796  dvaddxxbr  13798  dvimulf  13803  dvcj  13806  dvfre  13807  lgscllem  14041  lgsfle1  14043  lgsval4a  14056  lgsneg  14058  lgsdir  14069  lgsdilem2  14070  lgsdi  14071  lgsne0  14072  nninfall  14381  nninffeq  14392  refeq  14399  trilpolemclim  14407  trilpolemcl  14408  trilpolemisumle  14409  trilpolemeq1  14411  iswomni0  14422
  Copyright terms: Public domain W3C validator