Theorem frnd 6678

Description: Deduction form of frn 6677. 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 6677	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3911  ran crn 5632  ⟶wf 6495

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 207  df-an 396  df-f 6503

This theorem is referenced by:  f1un  6802  fliftrel  7265  f1iun  7902  f1dmex  7915  fo2ndf  8077  onoviun  8289  onnseq  8290  smores2  8300  domdifsn  9001  omxpenlem  9019  fodomr  9069  domss2  9077  f1domfi  9122  sucdom2  9144  f1finf1o  9192  f1finf1oOLD  9193  infn0  9227  f1fi  9239  fodomfir  9255  unirnffid  9274  intrnfi  9343  dffi3  9358  ordtypelem8  9454  ordtypelem9  9455  ordtypelem10  9456  hartogslem1  9471  brwdom2  9502  unxpwdom2  9517  ixpiunwdom  9519  infdifsn  9586  cantnf  9622  ac10ct  9963  numacn  9978  infpwfien  9991  fictb  10173  isf34lem5  10307  isf34lem7  10308  isf34lem6  10309  enfin1ai  10313  canthp1lem2  10582  gch3  10605  wuncval2  10676  peano5nni  12165  hashimarn  14381  hashf1lem1  14396  hashf1lem2  14397  ccatrn  14530  swrdrn  14593  pfxrn  14626  cshwrn  14743  limsupgle  15419  limsupgre  15423  isercolllem2  15608  isercoll  15610  isercoll2  15611  climsup  15612  ruclem11  16184  4sqlem11  16902  vdwapf  16919  vdwlem11  16938  0ram  16967  funcres2b  17839  funcres2c  17845  setcepi  18030  yoniso  18226  isacs4lem  18485  mgmhmima  18624  mhmima  18734  gsumwspan  18755  frmdss2  18772  cycsubm  19116  cycsubgcl  19120  cycsubgss  19121  ghmrn  19143  conjnmz  19166  ghmqusnsg  19196  ghmquskerlem3  19200  cntzmhm  19255  f1omvdconj  19360  odf1o2  19487  pgpssslw  19528  sylow2blem1  19534  lsmssv  19557  smndlsmidm  19570  pj1ghm2  19618  efgsp1  19651  efgrelexlemb  19664  cntzcmnf  19759  cyggenod  19798  gsumval3eu  19818  gsumval3lem2  19820  gsumval3  19821  gsumzsubmcl  19832  gsumzaddlem  19835  gsumzadd  19836  gsumzsplit  19841  gsumconst  19848  gsumzoppg  19858  gsumpt  19876  dmdprdd  19915  dprdfcntz  19931  dprdfeq0  19938  dprdlub  19942  dprdres  19944  dprdss  19945  dprdz  19946  subgdprd  19951  dprd2dlem1  19957  dprd2da  19958  dmdprdsplit2lem  19961  dpjghm2  19980  ablfac1b  19986  lmhmlsp  20988  pj1lmhm2  21040  pjfo  21657  frlmsplit2  21715  frlmsslsp  21738  frlmlbs  21739  frlmup3  21742  frlmup4  21743  lindff1  21762  lindfrn  21763  f1lindf  21764  indlcim  21782  aspval2  21840  mplcoe5lem  21979  mplbas2  21982  mplind  22010  evlslem1  22022  evlseu  22023  gsumply1subr  22151  m2cpmf1  22663  m2cpmghm  22664  iinopn  22822  pptbas  22928  tgrest  23079  resttopon  23081  rest0  23089  restfpw  23099  ordtbaslem  23108  ordtuni  23110  ordtbas2  23111  ordtrest  23122  ordtrest2  23124  cnclsi  23192  cnrest2r  23207  cnprest2  23210  lmss  23218  cncmp  23312  rncmp  23316  discmp  23318  connima  23345  conncn  23346  2ndcdisj  23376  2ndcomap  23378  dis2ndc  23380  lly1stc  23416  comppfsc  23452  kgencmp  23465  1stckgenlem  23473  kgencn3  23478  ptbasfi  23501  txbasval  23526  upxp  23543  uptx  23545  txtube  23560  txcmplem1  23561  txcmplem2  23562  tx1stc  23570  xkoptsub  23574  xkoco2cn  23578  xkococnlem  23579  hmeores  23691  fbasrn  23804  trfilss  23809  trfg  23811  uzrest  23817  rnelfmlem  23872  fclscmpi  23949  alexsublem  23964  ptcmplem1  23972  ptcmplem3  23974  cnextcn  23987  tmdgsum2  24016  subgtgp  24025  subgntr  24027  opnsubg  24028  clsnsg  24030  tgpconncomp  24033  tsmsfbas  24048  prdsdsf  24288  prdsxmetlem  24289  prdsmet  24291  imasdsf1olem  24294  unirnblps  24340  unirnbl  24341  prdsbl  24412  met1stc  24442  met2ndci  24443  prdsxmslem2  24450  xrge0gsumle  24755  xrge0tsms  24756  metdcn2  24761  metdsf  24770  metdsge  24771  cnmptre  24854  bndth  24890  evth  24891  evth2  24892  lebnumlem2  24894  lebnumlem3  24895  reparphti  24929  reparphtiOLD  24930  bcthlem5  25261  minveclem1  25357  minveclem3b  25361  evthicc2  25394  ovolmge0  25411  ovollb  25413  ovolgelb  25414  ovollb2lem  25422  ovollb2  25423  ovolunlem1a  25430  ovolunlem1  25431  ovoliunlem1  25436  ovoliun  25439  ovoliun2  25440  ovolscalem1  25447  ovolicc1  25450  ovolicc2lem4  25454  ovolicc2  25456  voliunlem2  25485  voliunlem3  25486  ioombl1lem2  25493  ioombl1lem4  25495  uniioovol  25513  uniiccvol  25514  uniioombllem1  25515  uniioombllem2  25517  uniioombllem3  25519  uniioombllem6  25522  uniioombl  25523  volsup2  25539  vitalilem2  25543  vitalilem4  25545  vitalilem5  25546  mbfsup  25598  mbfinf  25599  mbflimsup  25600  i1fima  25612  i1fima2  25613  itg1cl  25619  itg1ge0  25620  i1fmullem  25628  i1fadd  25629  i1fmul  25630  itg1addlem4  25633  itg1addlem5  25634  i1fmulc  25637  itg1mulc  25638  i1fres  25639  itg10a  25644  itg1ge0a  25645  itg1climres  25648  mbfi1fseqlem4  25652  itg2seq  25676  itg2monolem1  25684  itg2monolem2  25685  itg2monolem3  25686  itg2mono  25687  itg2i1fseq2  25690  itg2gt0  25694  itg2cnlem1  25695  itg2cn  25697  dvne0  25949  lhop2  25953  mdegleb  26002  mdegldg  26004  aalioulem3  26275  logccv  26605  efrlim  26912  efrlimOLD  26913  basellem3  27026  fsumvma  27157  lgseisenlem4  27322  noseqind  28226  uhgredgn0  29108  upgredgss  29112  umgredgss  29113  edgupgr  29114  upgredg  29117  usgruspgrb  29163  upgrres1  29293  ubthlem1  30849  minvecolem1  30853  htthlem  30896  ofrn  32613  ofrn2  32614  xppreima2  32625  fsumiunle  32804  ccatws1f1olast  32924  mgcf1o  32975  chnso  32986  gsumhashmul  33044  xrge0tsmsd  33045  symgcom  33055  cycpmcl  33088  cycpmco2lem1  33098  cycpmco2lem5  33102  cycpmco2  33105  cycpmconjv  33114  cycpmconjslem2  33127  elrgspnsubrunlem2  33215  idomsubr  33275  1arithidom  33501  ply1degltdimlem  33611  cmpcref  33833  ordtrestNEW  33904  ordtrest2NEW  33906  xrge0mulc1cn  33924  rge0scvg  33932  esumcst  34046  esumpfinvallem  34057  esumpcvgval  34061  esumiun  34077  omssubadd  34284  carsggect  34302  sibfinima  34323  sitgclg  34326  sitgaddlemb  34332  eulerpartgbij  34356  rrvrnss  34431  orvcval4  34445  erdsze2lem2  35184  cvxpconn  35222  cvxsconn  35223  cvmsss2  35254  cvmliftlem8  35272  cvmlift3lem6  35304  mrsubrn  35493  msubrn  35509  mvtss  35533  mclsssvlem  35542  mclsax  35549  mclsind  35550  neibastop2lem  36341  tailfb  36358  knoppcnlem10  36483  lindsdom  37601  poimirlem2  37609  poimirlem11  37618  poimirlem19  37626  poimirlem27  37634  poimirlem30  37637  mblfinlem2  37645  itg2addnclem2  37659  itg2gt0cn  37662  ftc1anclem3  37682  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anc  37688  cnresima  37751  istotbnd3  37758  sstotbnd2  37761  totbndbnd  37776  prdsbnd  37780  cntotbnd  37783  ismtyima  37790  heibor1lem  37796  heibor  37808  rrnequiv  37822  lsatlss  38982  cdleme50rnlem  40531  sticksstones2  42128  aks6d1c6lem5  42158  cmpfiiin  42678  isnacs3  42691  eldioph2lem2  42742  fnwe2lem2  43033  lmhmfgima  43066  cantnfub2  43304  onnog  43411  gneispacern  44120  imo72b2lem2  44149  imo72b2lem1  44151  imo72b2  44154  refsumcn  45017  cncmpmax  45019  elpmrn  45207  climinf  45597  climinf2lem  45697  limsupvaluz2  45729  supcnvlimsup  45731  limsupgtlem  45768  icccncfext  45878  dvsinax  45904  itgsubsticclem  45966  fourierdlem70  46167  fourierdlem82  46179  fge0npnf  46358  sge0resrnlem  46394  sge0isum  46418  sge0seq  46437  meadjiunlem  46456  omeiunle  46508  hoicvr  46539  vonvolmbllem  46651  preimaioomnf  46710  smfco  46793  ackvalsucsucval  48670  aacllem  49783