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

Theorem ffvelrnd 5335
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 5334 . 2 ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
41, 3mpdan 412 1 (𝜑 → (𝐹𝐶) ∈ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  wf 4928  cfv 4932
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-pow 3956  ax-pr 3972
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-v 2604  df-sbc 2817  df-un 2978  df-in 2980  df-ss 2987  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-opab 3848  df-id 4056  df-xp 4377  df-rel 4378  df-cnv 4379  df-co 4380  df-dm 4381  df-rn 4382  df-iota 4897  df-fun 4934  df-fn 4935  df-f 4936  df-fv 4940
This theorem is referenced by:  isotr  5487  caofinvl  5764  rdgon  6035  frecabcl  6048  phplem4dom  6397  fidceq  6404  dif1en  6414  fin0  6419  fin0or  6420  infm  6432  en2eqpr  6434  supisoti  6482  ordiso2  6505  cauappcvgprlemm  6897  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlem2  6912  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprlem2  6932  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnbj  6945  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgsrlemcau  7031  caucvgsrlemgt1  7033  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  caucvgsr  7040  axcaucvglemval  7125  axcaucvglemcau  7126  axcaucvglemres  7127  fseq1p1m1  9187  4fvwrd4  9227  fvinim0ffz  9327  frecuzrdgg  9498  frecuzrdgsuctlem  9505  iseqvalt  9532  iseqcl  9537  iseqp1t  9539  sizefz1  9807  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemf  10007  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniqlem  10018  resqrexlemdecn  10036  resqrexlemcalc3  10040  resqrexlemnmsq  10041  resqrexlemnm  10042  resqrexlemcvg  10043  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemga  10047  clim2iser  10313  clim2iser2  10314  climrecvg1n  10323  climcvg1nlem  10324  serif0  10327  sumeq2d  10334  sumeq2  10335  fisumcvg  10338  nn0seqcvgd  10567  ialgrlem1st  10568
  Copyright terms: Public domain W3C validator