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

Theorem ffvelrnda 5521
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
StepHypRef Expression
1 ffvelrnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffvelrn 5519 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
31, 2sylan 279 1 ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1463  wf 5087  cfv 5091
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-sbc 2881  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099
This theorem is referenced by:  ffvelrnd  5522  f1ocnvdm  5648  foeqcnvco  5657  f1oiso2  5694  offeq  5961  suppssof1  5965  ofco  5966  caofref  5969  caofinvl  5970  caofcom  5971  caofrss  5972  caoftrn  5973  smofvon2dm  6159  smofvon  6162  mapxpen  6708  xpmapenlem  6709  en2eqpr  6767  supisoex  6862  ordiso2  6886  omp1eomlem  6945  ctssdccl  6962  ctssdc  6964  enumctlemm  6965  enomnilem  6976  fodjuomnilemdc  6982  ismkvnex  6995  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemladdrl  7450  caucvgprprlemopu  7471  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  caucvgsrlemcl  7561  caucvgsrlemfv  7563  caucvgsrlemcau  7565  caucvgsrlembound  7566  caucvgsrlemoffval  7568  caucvgsrlemofff  7569  caucvgsrlemoffgt1  7571  caucvgsrlemoffres  7572  caucvgsr  7574  axcaucvglemcl  7667  frecuzrdgfunlem  10143  monoord2  10201  seq3f1o  10228  seq3homo  10234  seqfeq3  10236  zfz1isolemiso  10533  seq3coll  10536  resqrexlemfp1  10732  resqrexlemover  10733  resqrexlemdec  10734  resqrexlemlo  10736  resqrexlemcalc1  10737  resqrexlemcalc2  10738  resqrexlemcalc3  10739  resqrexlemgt0  10743  resqrexlemsqa  10747  clim2ser  11057  clim2ser2  11058  isermulc2  11060  iserle  11062  climserle  11065  climrecvg1n  11068  climcvg1nlem  11069  summodclem3  11100  summodclem2a  11101  fsumgcl  11106  fsum3  11107  fsumf1o  11110  isumss  11111  fisumss  11112  fsumcl2lem  11118  fsumadd  11126  isumclim3  11143  isummulc2  11146  isumrecl  11149  isumadd  11151  fsummulc2  11168  iserabs  11195  cvgcmpub  11196  isumshft  11210  isumsplit  11211  mertensabs  11257  efcj  11289  nn0seqcvgd  11629  algrp1  11634  alginv  11635  algcvg  11636  algcvga  11639  algfx  11640  eucalgcvga  11646  cnptoprest2  12315  lmss  12321  txcnmpt  12348  txlm  12354  lmcn2  12355  psmetxrge0  12407  metcnp  12587  climcncf  12646  negfcncf  12664  ivthdec  12697  dvcnp2cntop  12738  dvaddxxbr  12740  dvimulf  12745  dvcj  12748  dvfre  12749  nninfall  13038  nninffeq  13050  refeq  13057  trilpolemclim  13063  trilpolemcl  13064  trilpolemisumle  13065  trilpolemeq1  13067
  Copyright terms: Public domain W3C validator