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

Theorem ffvelrnda 5418
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 5416 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
31, 2sylan 277 1 ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  wf 4998  cfv 5002
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2839  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-fv 5010
This theorem is referenced by:  ffvelrnd  5419  f1ocnvdm  5542  foeqcnvco  5551  f1oiso2  5588  suppssof1  5854  ofco  5855  caofref  5858  caofinvl  5859  caofcom  5860  caofrss  5861  caoftrn  5862  smofvon2dm  6043  smofvon  6046  mapxpen  6544  xpmapenlem  6545  en2eqpr  6603  supisoex  6683  ordiso2  6707  enomnilem  6773  fodjuomnilemdc  6778  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemladdrl  7216  caucvgprprlemopu  7237  caucvgprprlemexbt  7244  caucvgprprlemexb  7245  caucvgsrlemcl  7313  caucvgsrlemfv  7315  caucvgsrlemcau  7317  caucvgsrlembound  7318  caucvgsrlemoffval  7320  caucvgsrlemofff  7321  caucvgsrlemoffgt1  7323  caucvgsrlemoffres  7324  caucvgsr  7326  axcaucvglemcl  7409  frecuzrdgfunlem  9791  monoord2  9870  seq3f1o  9898  seq3homo  9909  zfz1isolemiso  10209  iseqcoll  10212  resqrexlemfp1  10407  resqrexlemover  10408  resqrexlemdec  10409  resqrexlemlo  10411  resqrexlemcalc1  10412  resqrexlemcalc2  10413  resqrexlemcalc3  10414  resqrexlemgt0  10418  resqrexlemsqa  10422  clim2ser  10689  clim2ser2  10690  iisermulc2  10692  iserle  10695  climserle  10698  climrecvg1n  10701  climcvg1nlem  10702  isummolem3  10734  isummolem2a  10735  fsumgcl  10741  fisum  10742  fsumf1o  10746  isumss  10747  fisumss  10748  fsumcl2lem  10755  fsumadd  10763  isumclim3  10780  isummulc2  10783  isumrecl  10786  isumadd  10788  fsummulc2  10805  cvgcmpub  10832  isumshft  10846  isumsplit  10847  nn0seqcvgd  11116  ialginv  11122  ialgcvg  11123  ialgcvga  11126  ialgfx  11127  eucialgcvga  11133  nninfall  11557
  Copyright terms: Public domain W3C validator