Theorem frnd 6714

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

Syntax hints:   → wi 4   ⊆ wss 3905  ran crn 5662  ⟶wf 6532

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 210  df-an 401  df-f 6540

This theorem is referenced by:  f1un  6841  fliftrel  7306  f1iun  7937  f1dmex  7950  fo2ndf  8112  onoviun  8326  onnseq  8327  smores2  8337  domdifsn  9044  omxpenlem  9062  fodomr  9112  domss2  9120  f1domfi  9161  sucdom2  9183  f1finf1o  9229  infn0  9258  f1fi  9270  fodomfir  9283  unirnffid  9300  intrnfi  9372  dffi3  9387  ordtypelem8  9483  ordtypelem9  9484  ordtypelem10  9485  hartogslem1  9500  brwdom2  9531  unxpwdom2  9546  ixpiunwdom  9548  infdifsn  9622  cantnf  9658  ac10ct  10014  numacn  10029  infpwfien  10042  fictb  10223  isf34lem5  10357  isf34lem7  10358  isf34lem6  10359  enfin1ai  10363  canthp1lem2  10633  gch3  10656  wuncval2  10727  peano5nni  12231  hashimarn  14473  hashf1lem1  14488  hashf1lem2  14489  ccatrn  14623  swrdrn  14686  pfxrn  14719  cshwrn  14835  limsupgle  15524  limsupgre  15528  isercolllem2  15713  isercoll  15715  isercoll2  15716  climsup  15717  ruclem11  16291  4sqlem11  17010  vdwapf  17027  vdwlem11  17046  0ram  17075  funcres2b  17949  funcres2c  17955  setcepi  18140  yoniso  18336  isacs4lem  18595  chnso  18675  mgmhmima  18768  mhmima  18879  gsumwspan  18900  frmdss2  18917  cycsubm  19268  cycsubgcl  19272  cycsubgss  19273  ghmrn  19294  conjnmz  19317  ghmqusnsg  19347  ghmquskerlem3  19351  cntzmhm  19406  f1omvdconj  19511  odf1o2  19638  pgpssslw  19679  sylow2blem1  19685  lsmssv  19708  smndlsmidm  19721  pj1ghm2  19769  efgsp1  19802  efgrelexlemb  19815  cntzcmnf  19910  cyggenod  19949  gsumval3eu  19969  gsumval3lem2  19971  gsumval3  19972  gsumzsubmcl  19983  gsumzaddlem  19986  gsumzadd  19987  gsumzsplit  19992  gsumconst  19999  gsumzoppg  20009  gsumpt  20027  dmdprdd  20066  dprdfcntz  20082  dprdfeq0  20089  dprdlub  20093  dprdres  20095  dprdss  20096  dprdz  20097  subgdprd  20102  dprd2dlem1  20108  dprd2da  20109  dmdprdsplit2lem  20112  dpjghm2  20131  ablfac1b  20137  lmhmlsp  21170  pj1lmhm2  21222  pjfo  21865  frlmsplit2  21923  frlmsslsp  21946  frlmlbs  21947  frlmup3  21950  frlmup4  21951  lindff1  21970  lindfrn  21971  f1lindf  21972  indlcim  21990  aspval2  22048  mplcoe5lem  22190  mplbas2  22193  mplind  22221  evlslem1  22233  evlseu  22234  gsumply1subr  22393  m2cpmf1  22900  m2cpmghm  22901  iinopn  23059  pptbas  23165  tgrest  23316  resttopon  23318  rest0  23326  restfpw  23336  ordtbaslem  23345  ordtuni  23347  ordtbas2  23348  ordtrest  23359  ordtrest2  23361  cnclsi  23429  cnrest2r  23444  cnprest2  23447  lmss  23455  cncmp  23549  rncmp  23553  discmp  23555  connima  23582  conncn  23583  2ndcdisj  23613  2ndcomap  23615  dis2ndc  23617  lly1stc  23653  comppfsc  23689  kgencmp  23702  1stckgenlem  23710  kgencn3  23715  ptbasfi  23738  txbasval  23763  upxp  23780  uptx  23782  txtube  23797  txcmplem1  23798  txcmplem2  23799  tx1stc  23807  xkoptsub  23811  xkoco2cn  23815  xkococnlem  23816  hmeores  23928  fbasrn  24041  trfilss  24046  trfg  24048  uzrest  24054  rnelfmlem  24109  fclscmpi  24186  alexsublem  24201  ptcmplem1  24209  ptcmplem3  24211  cnextcn  24224  tmdgsum2  24253  subgtgp  24262  subgntr  24264  opnsubg  24265  clsnsg  24267  tgpconncomp  24270  tsmsfbas  24285  prdsdsf  24524  prdsxmetlem  24525  prdsmet  24527  imasdsf1olem  24530  unirnblps  24576  unirnbl  24577  prdsbl  24648  met1stc  24678  met2ndci  24679  prdsxmslem2  24686  xrge0gsumle  24991  xrge0tsms  24992  metdcn2  24997  metdsf  25006  metdsge  25007  cnmptre  25086  bndth  25117  evth  25118  evth2  25119  lebnumlem2  25121  lebnumlem3  25122  reparphti  25156  bcthlem5  25487  minveclem1  25583  minveclem3b  25587  evthicc2  25619  ovolmge0  25636  ovollb  25638  ovolgelb  25639  ovollb2lem  25647  ovollb2  25648  ovolunlem1a  25655  ovolunlem1  25656  ovoliunlem1  25661  ovoliun  25664  ovoliun2  25665  ovolscalem1  25672  ovolicc1  25675  ovolicc2lem4  25679  ovolicc2  25681  voliunlem2  25710  voliunlem3  25711  ioombl1lem2  25718  ioombl1lem4  25720  uniioovol  25738  uniiccvol  25739  uniioombllem1  25740  uniioombllem2  25742  uniioombllem3  25744  uniioombllem6  25747  uniioombl  25748  volsup2  25764  vitalilem2  25768  vitalilem4  25770  vitalilem5  25771  mbfsup  25823  mbfinf  25824  mbflimsup  25825  i1fima  25837  i1fima2  25838  itg1cl  25844  itg1ge0  25845  i1fmullem  25853  i1fadd  25854  i1fmul  25855  itg1addlem4  25858  itg1addlem5  25859  i1fmulc  25862  itg1mulc  25863  i1fres  25864  itg10a  25869  itg1ge0a  25870  itg1climres  25873  mbfi1fseqlem4  25877  itg2seq  25901  itg2monolem1  25909  itg2monolem2  25910  itg2monolem3  25911  itg2mono  25912  itg2i1fseq2  25915  itg2gt0  25919  itg2cnlem1  25920  itg2cn  25922  dvne0  26170  lhop2  26174  mdegleb  26221  mdegldg  26223  aalioulem3  26497  logccv  26828  efrlim  27134  basellem3  27247  fsumvma  27377  lgseisenlem4  27542  noseqind  28485  uhgredgn0  29478  upgredgss  29482  umgredgss  29483  edgupgr  29484  upgredg  29487  usgruspgrb  29533  upgrres1  29663  ubthlem1  31222  minvecolem1  31226  htthlem  31269  ofrn  32984  ofrn2  32985  xppreima2  32996  fsumiunle  33173  ccatws1f1olast  33272  mgcf1o  33323  gsumhashmul  33387  xrge0tsmsd  33393  symgcom  33403  cycpmcl  33436  cycpmco2lem1  33446  cycpmco2lem5  33450  cycpmco2  33453  cycpmconjv  33462  cycpmconjslem2  33475  elrgspnsubrunlem2  33568  idomsubr  33630  1arithidom  33827  psrbasfsupp  33901  esplyfv  33960  esplyfval3  33962  ply1degltdimlem  34012  cmpcref  34240  ordtrestNEW  34311  ordtrest2NEW  34313  xrge0mulc1cn  34331  rge0scvg  34339  esumcst  34453  esumpfinvallem  34464  esumpcvgval  34468  esumiun  34484  omssubadd  34690  carsggect  34708  sibfinima  34729  sitgclg  34732  sitgaddlemb  34738  eulerpartgbij  34762  rrvrnss  34837  orvcval4  34851  erdsze2lem2  35696  cvxpconn  35734  cvxsconn  35735  cvmsss2  35766  cvmliftlem8  35784  cvmlift3lem6  35816  mrsubrn  36005  msubrn  36021  mvtss  36045  mclsssvlem  36054  mclsax  36061  mclsind  36062  neibastop2lem  36891  tailfb  36908  knoppcnlem10  37111  lindsdom  38285  poimirlem2  38293  poimirlem11  38302  poimirlem19  38310  poimirlem27  38318  poimirlem30  38321  mblfinlem2  38329  itg2addnclem2  38343  itg2gt0cn  38346  ftc1anclem3  38366  ftc1anclem6  38369  ftc1anclem7  38370  ftc1anc  38372  cnresima  38435  istotbnd3  38442  sstotbnd2  38445  totbndbnd  38460  prdsbnd  38464  cntotbnd  38467  ismtyima  38474  heibor1lem  38480  heibor  38492  rrnequiv  38506  lsatlss  39790  cdleme50rnlem  41338  sticksstones2  42934  aks6d1c6lem5  42964  cmpfiiin  43448  isnacs3  43461  eldioph2lem2  43512  fnwe2lem2  43798  lmhmfgima  43831  cantnfub2  44069  onnoxpg  44175  gneispacern  44884  imo72b2lem2  44913  imo72b2lem1  44915  imo72b2  44918  refsumcn  45770  cncmpmax  45772  elpmrn  45956  climinf  46342  climinf2lem  46440  limsupvaluz2  46472  supcnvlimsup  46474  limsupgtlem  46511  icccncfext  46621  dvsinax  46647  itgsubsticclem  46709  fourierdlem70  46910  fourierdlem82  46922  fourierdlem113  46953  fge0npnf  47101  sge0resrnlem  47137  sge0isum  47161  sge0seq  47180  meadjiunlem  47199  omeiunle  47251  hoicvr  47282  vonvolmbllem  47394  preimaioomnf  47453  smfco  47536  chnsubseqwl  47615  ackvalsucsucval  49488  aacllem  50641