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

Theorem ffvelrnd 5400
Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
ffvelrnd.1 (𝜑𝐹:𝐴𝐵)
ffvelrnd.2 (𝜑𝐶𝐴)
Assertion
Ref Expression
ffvelrnd (𝜑 → (𝐹𝐶) ∈ 𝐵)

Proof of Theorem ffvelrnd
StepHypRef Expression
1 ffvelrnd.2 . 2 (𝜑𝐶𝐴)
2 ffvelrnd.1 . . 3 (𝜑𝐹:𝐴𝐵)
32ffvelrnda 5399 . 2 ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
41, 3mpdan 412 1 (𝜑 → (𝐹𝐶) ∈ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  wf 4979  cfv 4983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-sbc 2830  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-opab 3877  df-id 4096  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-fv 4991
This theorem is referenced by:  isotr  5558  caofinvl  5836  rdgon  6107  frecabcl  6120  phplem4dom  6532  fidceq  6539  dif1en  6549  fin0  6555  fin0or  6556  infm  6574  en2eqpr  6577  supisoti  6652  ordiso2  6675  updjudhcoinlf  6718  updjudhcoinrg  6719  enomnilem  6741  finomni  6743  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  cauappcvgprlemm  7151  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlem2  7166  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemm  7174  caucvgprlemloc  7181  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgprlem2  7186  caucvgprprlemnkltj  7195  caucvgprprlemnkeqj  7196  caucvgprprlemnbj  7199  caucvgprprlemmu  7201  caucvgprprlemopl  7203  caucvgprprlemloc  7209  caucvgprprlemexbt  7212  caucvgprprlemexb  7213  caucvgprprlemaddq  7214  caucvgprprlem1  7215  caucvgprprlem2  7216  caucvgsrlemcau  7285  caucvgsrlemgt1  7287  caucvgsrlemoffcau  7290  caucvgsrlemoffres  7292  caucvgsr  7294  axcaucvglemval  7379  axcaucvglemcau  7380  axcaucvglemres  7381  fseq1p1m1  9441  4fvwrd4  9482  fvinim0ffz  9583  frecuzrdgg  9754  frecuzrdgsuctlem  9761  iseqvalt  9804  iseqcl  9811  iseqp1t  9813  iseqf1olemkle  9837  iseqf1olemklt  9838  iseqf1olemqcl  9839  iseqf1olemnab  9841  iseqf1olemmo  9845  iseqf1olemqk  9847  iseqf1olemjpcl  9848  iseqf1olemqpcl  9849  iseqf1olemfvp  9850  iseqf1olemqsumkj  9851  iseqf1olemqsumk  9852  iseqf1olemqsum  9853  iseqf1olemstep  9854  iseqf1oleml  9856  iseqf1o  9857  ser3ge0  9872  ser3le  9873  hashfz1  10109  resunimafz0  10154  leisorel  10160  zfz1isolemiso  10162  iseqcoll  10165  caucvgrelemcau  10330  caucvgre  10331  cvg1nlemf  10333  cvg1nlemcau  10334  cvg1nlemres  10335  recvguniqlem  10344  resqrexlemdecn  10362  resqrexlemcalc3  10366  resqrexlemnmsq  10367  resqrexlemnm  10368  resqrexlemcvg  10369  resqrexlemoverl  10371  resqrexlemglsq  10372  resqrexlemga  10373  clim2iser  10641  clim2iser2  10642  climrecvg1n  10651  climcvg1nlem  10652  serif0  10655  sumeq2  10662  fisumcvg  10680  isummolem2a  10684  fisumss  10694  fsumcl2lem  10699  fsumadd  10707  nn0seqcvgd  10948  ialgrlem1st  10949  nnsf  11383  peano4nninf  11384  nninfalllem1  11387  nninfsellemdc  11390  nninfsellemeq  11394  nninfsellemqall  11395  nninfsellemeqinf  11396  nninfomnilem  11398
  Copyright terms: Public domain W3C validator