Theorem frnd 6700

Description: Deduction form of frn 6699. The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
frnd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
frnd	⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frnd

Step	Hyp	Ref	Expression
1		frnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		frn 6699	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3904  ran crn 5648  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400  df-f 6525

This theorem is referenced by:  f1un  6827  fliftrel  7292  f1iun  7925  f1dmex  7938  fo2ndf  8100  onoviun  8314  onnseq  8315  smores2  8325  domdifsn  9032  omxpenlem  9050  fodomr  9100  domss2  9108  f1domfi  9149  sucdom2  9171  f1finf1o  9217  infn0  9246  f1fi  9258  fodomfir  9272  unirnffid  9290  intrnfi  9362  dffi3  9377  ordtypelem8  9473  ordtypelem9  9474  ordtypelem10  9475  hartogslem1  9490  brwdom2  9521  unxpwdom2  9536  ixpiunwdom  9538  infdifsn  9612  cantnf  9648  ac10ct  9990  numacn  10005  infpwfien  10018  fictb  10200  isf34lem5  10335  isf34lem7  10336  isf34lem6  10337  enfin1ai  10341  canthp1lem2  10611  gch3  10634  wuncval2  10705  peano5nni  12213  hashimarn  14453  hashf1lem1  14468  hashf1lem2  14469  ccatrn  14603  swrdrn  14666  pfxrn  14699  cshwrn  14815  limsupgle  15504  limsupgre  15508  isercolllem2  15693  isercoll  15695  isercoll2  15696  climsup  15697  ruclem11  16272  4sqlem11  16991  vdwapf  17008  vdwlem11  17027  0ram  17056  funcres2b  17930  funcres2c  17936  setcepi  18121  yoniso  18317  isacs4lem  18576  chnso  18656  mgmhmima  18749  mhmima  18859  gsumwspan  18880  frmdss2  18897  cycsubm  19243  cycsubgcl  19247  cycsubgss  19248  ghmrn  19269  conjnmz  19292  ghmqusnsg  19322  ghmquskerlem3  19326  cntzmhm  19381  f1omvdconj  19486  odf1o2  19613  pgpssslw  19654  sylow2blem1  19660  lsmssv  19683  smndlsmidm  19696  pj1ghm2  19744  efgsp1  19777  efgrelexlemb  19790  cntzcmnf  19885  cyggenod  19924  gsumval3eu  19944  gsumval3lem2  19946  gsumval3  19947  gsumzsubmcl  19958  gsumzaddlem  19961  gsumzadd  19962  gsumzsplit  19967  gsumconst  19974  gsumzoppg  19984  gsumpt  20002  dmdprdd  20041  dprdfcntz  20057  dprdfeq0  20064  dprdlub  20068  dprdres  20070  dprdss  20071  dprdz  20072  subgdprd  20077  dprd2dlem1  20083  dprd2da  20084  dmdprdsplit2lem  20087  dpjghm2  20106  ablfac1b  20112  lmhmlsp  21116  pj1lmhm2  21168  pjfo  21767  frlmsplit2  21825  frlmsslsp  21848  frlmlbs  21849  frlmup3  21852  frlmup4  21853  lindff1  21872  lindfrn  21873  f1lindf  21874  indlcim  21892  aspval2  21950  mplcoe5lem  22092  mplbas2  22095  mplind  22123  evlslem1  22135  evlseu  22136  gsumply1subr  22295  m2cpmf1  22803  m2cpmghm  22804  iinopn  22962  pptbas  23068  tgrest  23219  resttopon  23221  rest0  23229  restfpw  23239  ordtbaslem  23248  ordtuni  23250  ordtbas2  23251  ordtrest  23262  ordtrest2  23264  cnclsi  23332  cnrest2r  23347  cnprest2  23350  lmss  23358  cncmp  23452  rncmp  23456  discmp  23458  connima  23485  conncn  23486  2ndcdisj  23516  2ndcomap  23518  dis2ndc  23520  lly1stc  23556  comppfsc  23592  kgencmp  23605  1stckgenlem  23613  kgencn3  23618  ptbasfi  23641  txbasval  23666  upxp  23683  uptx  23685  txtube  23700  txcmplem1  23701  txcmplem2  23702  tx1stc  23710  xkoptsub  23714  xkoco2cn  23718  xkococnlem  23719  hmeores  23831  fbasrn  23944  trfilss  23949  trfg  23951  uzrest  23957  rnelfmlem  24012  fclscmpi  24089  alexsublem  24104  ptcmplem1  24112  ptcmplem3  24114  cnextcn  24127  tmdgsum2  24156  subgtgp  24165  subgntr  24167  opnsubg  24168  clsnsg  24170  tgpconncomp  24173  tsmsfbas  24188  prdsdsf  24427  prdsxmetlem  24428  prdsmet  24430  imasdsf1olem  24433  unirnblps  24479  unirnbl  24480  prdsbl  24551  met1stc  24581  met2ndci  24582  prdsxmslem2  24589  xrge0gsumle  24894  xrge0tsms  24895  metdcn2  24900  metdsf  24909  metdsge  24910  cnmptre  24989  bndth  25020  evth  25021  evth2  25022  lebnumlem2  25024  lebnumlem3  25025  reparphti  25059  bcthlem5  25390  minveclem1  25486  minveclem3b  25490  evthicc2  25522  ovolmge0  25539  ovollb  25541  ovolgelb  25542  ovollb2lem  25550  ovollb2  25551  ovolunlem1a  25558  ovolunlem1  25559  ovoliunlem1  25564  ovoliun  25567  ovoliun2  25568  ovolscalem1  25575  ovolicc1  25578  ovolicc2lem4  25582  ovolicc2  25584  voliunlem2  25613  voliunlem3  25614  ioombl1lem2  25621  ioombl1lem4  25623  uniioovol  25641  uniiccvol  25642  uniioombllem1  25643  uniioombllem2  25645  uniioombllem3  25647  uniioombllem6  25650  uniioombl  25651  volsup2  25667  vitalilem2  25671  vitalilem4  25673  vitalilem5  25674  mbfsup  25726  mbfinf  25727  mbflimsup  25728  i1fima  25740  i1fima2  25741  itg1cl  25747  itg1ge0  25748  i1fmullem  25756  i1fadd  25757  i1fmul  25758  itg1addlem4  25761  itg1addlem5  25762  i1fmulc  25765  itg1mulc  25766  i1fres  25767  itg10a  25772  itg1ge0a  25773  itg1climres  25776  mbfi1fseqlem4  25780  itg2seq  25804  itg2monolem1  25812  itg2monolem2  25813  itg2monolem3  25814  itg2mono  25815  itg2i1fseq2  25818  itg2gt0  25822  itg2cnlem1  25823  itg2cn  25825  dvne0  26073  lhop2  26077  mdegleb  26124  mdegldg  26126  aalioulem3  26398  logccv  26728  efrlim  27034  basellem3  27147  fsumvma  27277  lgseisenlem4  27442  noseqind  28385  uhgredgn0  29329  upgredgss  29333  umgredgss  29334  edgupgr  29335  upgredg  29338  usgruspgrb  29384  upgrres1  29514  ubthlem1  31073  minvecolem1  31077  htthlem  31120  ofrn  32841  ofrn2  32842  xppreima2  32853  fsumiunle  33031  ccatws1f1olast  33130  mgcf1o  33181  gsumhashmul  33247  xrge0tsmsd  33253  symgcom  33263  cycpmcl  33296  cycpmco2lem1  33306  cycpmco2lem5  33310  cycpmco2  33313  cycpmconjv  33322  cycpmconjslem2  33335  elrgspnsubrunlem2  33429  idomsubr  33496  1arithidom  33733  psrbasfsupp  33808  esplyfv  33867  esplyfval3  33869  ply1degltdimlem  33919  cmpcref  34147  ordtrestNEW  34218  ordtrest2NEW  34220  xrge0mulc1cn  34238  rge0scvg  34246  esumcst  34360  esumpfinvallem  34371  esumpcvgval  34375  esumiun  34391  omssubadd  34597  carsggect  34615  sibfinima  34636  sitgclg  34639  sitgaddlemb  34645  eulerpartgbij  34669  rrvrnss  34744  orvcval4  34758  erdsze2lem2  35554  cvxpconn  35592  cvxsconn  35593  cvmsss2  35624  cvmliftlem8  35642  cvmlift3lem6  35674  mrsubrn  35863  msubrn  35879  mvtss  35903  mclsssvlem  35912  mclsax  35919  mclsind  35920  neibastop2lem  36720  tailfb  36737  knoppcnlem10  36940  lindsdom  38113  poimirlem2  38121  poimirlem11  38130  poimirlem19  38138  poimirlem27  38146  poimirlem30  38149  mblfinlem2  38157  itg2addnclem2  38171  itg2gt0cn  38174  ftc1anclem3  38194  ftc1anclem6  38197  ftc1anclem7  38198  ftc1anc  38200  cnresima  38263  istotbnd3  38270  sstotbnd2  38273  totbndbnd  38288  prdsbnd  38292  cntotbnd  38295  ismtyima  38302  heibor1lem  38308  heibor  38320  rrnequiv  38334  lsatlss  39620  cdleme50rnlem  41168  sticksstones2  42764  aks6d1c6lem5  42794  cmpfiiin  43278  isnacs3  43291  eldioph2lem2  43342  fnwe2lem2  43628  lmhmfgima  43661  cantnfub2  43899  onnoxpg  44005  gneispacern  44714  imo72b2lem2  44743  imo72b2lem1  44745  imo72b2  44748  refsumcn  45610  cncmpmax  45612  elpmrn  45796  climinf  46182  climinf2lem  46280  limsupvaluz2  46312  supcnvlimsup  46314  limsupgtlem  46351  icccncfext  46461  dvsinax  46487  itgsubsticclem  46549  fourierdlem70  46750  fourierdlem82  46762  fourierdlem113  46793  fge0npnf  46941  sge0resrnlem  46977  sge0isum  47001  sge0seq  47020  meadjiunlem  47039  omeiunle  47091  hoicvr  47122  vonvolmbllem  47234  preimaioomnf  47293  smfco  47376  chnsubseqwl  47455  ackvalsucsucval  49310  aacllem  50422