Theorem frnd 6744

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

Syntax hints:   → wi 4   ⊆ wss 3951  ran crn 5686  ⟶wf 6557

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 6565

This theorem is referenced by:  f1un  6868  fliftrel  7328  f1iun  7968  f1dmex  7981  fo2ndf  8146  onoviun  8383  onnseq  8384  smores2  8394  domdifsn  9094  omxpenlem  9113  sucdom2OLD  9122  fodomr  9168  domss2  9176  f1domfi  9221  sucdom2  9243  f1finf1o  9305  f1finf1oOLD  9306  infn0  9340  f1fi  9352  fodomfir  9368  unirnffid  9387  intrnfi  9456  dffi3  9471  ordtypelem8  9565  ordtypelem9  9566  ordtypelem10  9567  hartogslem1  9582  brwdom2  9613  unxpwdom2  9628  ixpiunwdom  9630  infdifsn  9697  cantnf  9733  ac10ct  10074  numacn  10089  infpwfien  10102  fictb  10284  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  enfin1ai  10424  canthp1lem2  10693  gch3  10716  wuncval2  10787  peano5nni  12269  hashimarn  14479  hashf1lem1  14494  hashf1lem2  14495  ccatrn  14627  swrdrn  14690  pfxrn  14723  cshwrn  14840  limsupgle  15513  limsupgre  15517  isercolllem2  15702  isercoll  15704  isercoll2  15705  climsup  15706  ruclem11  16276  4sqlem11  16993  vdwapf  17010  vdwlem11  17029  0ram  17058  funcres2b  17942  funcres2c  17948  setcepi  18133  yoniso  18330  isacs4lem  18589  mgmhmima  18728  mhmima  18838  gsumwspan  18859  frmdss2  18876  cycsubm  19220  cycsubgcl  19224  cycsubgss  19225  ghmrn  19247  conjnmz  19270  ghmqusnsg  19300  ghmquskerlem3  19304  cntzmhm  19359  f1omvdconj  19464  odf1o2  19591  pgpssslw  19632  sylow2blem1  19638  lsmssv  19661  smndlsmidm  19674  pj1ghm2  19722  efgsp1  19755  efgrelexlemb  19768  cntzcmnf  19863  cyggenod  19902  gsumval3eu  19922  gsumval3lem2  19924  gsumval3  19925  gsumzsubmcl  19936  gsumzaddlem  19939  gsumzadd  19940  gsumzsplit  19945  gsumconst  19952  gsumzoppg  19962  gsumpt  19980  dmdprdd  20019  dprdfcntz  20035  dprdfeq0  20042  dprdlub  20046  dprdres  20048  dprdss  20049  dprdz  20050  subgdprd  20055  dprd2dlem1  20061  dprd2da  20062  dmdprdsplit2lem  20065  dpjghm2  20084  ablfac1b  20090  lmhmlsp  21048  pj1lmhm2  21100  pjfo  21735  frlmsplit2  21793  frlmsslsp  21816  frlmlbs  21817  frlmup3  21820  frlmup4  21821  lindff1  21840  lindfrn  21841  f1lindf  21842  indlcim  21860  aspval2  21918  mplcoe5lem  22057  mplbas2  22060  mplind  22094  evlslem1  22106  evlseu  22107  gsumply1subr  22235  m2cpmf1  22749  m2cpmghm  22750  iinopn  22908  pptbas  23015  tgrest  23167  resttopon  23169  rest0  23177  restfpw  23187  ordtbaslem  23196  ordtuni  23198  ordtbas2  23199  ordtrest  23210  ordtrest2  23212  cnclsi  23280  cnrest2r  23295  cnprest2  23298  lmss  23306  cncmp  23400  rncmp  23404  discmp  23406  connima  23433  conncn  23434  2ndcdisj  23464  2ndcomap  23466  dis2ndc  23468  lly1stc  23504  comppfsc  23540  kgencmp  23553  1stckgenlem  23561  kgencn3  23566  ptbasfi  23589  txbasval  23614  upxp  23631  uptx  23633  txtube  23648  txcmplem1  23649  txcmplem2  23650  tx1stc  23658  xkoptsub  23662  xkoco2cn  23666  xkococnlem  23667  hmeores  23779  fbasrn  23892  trfilss  23897  trfg  23899  uzrest  23905  rnelfmlem  23960  fclscmpi  24037  alexsublem  24052  ptcmplem1  24060  ptcmplem3  24062  cnextcn  24075  tmdgsum2  24104  subgtgp  24113  subgntr  24115  opnsubg  24116  clsnsg  24118  tgpconncomp  24121  tsmsfbas  24136  prdsdsf  24377  prdsxmetlem  24378  prdsmet  24380  imasdsf1olem  24383  unirnblps  24429  unirnbl  24430  prdsbl  24504  met1stc  24534  met2ndci  24535  prdsxmslem2  24542  xrge0gsumle  24855  xrge0tsms  24856  metdcn2  24861  metdsf  24870  metdsge  24871  cnmptre  24954  bndth  24990  evth  24991  evth2  24992  lebnumlem2  24994  lebnumlem3  24995  reparphti  25029  reparphtiOLD  25030  bcthlem5  25362  minveclem1  25458  minveclem3b  25462  evthicc2  25495  ovolmge0  25512  ovollb  25514  ovolgelb  25515  ovollb2lem  25523  ovollb2  25524  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun  25540  ovoliun2  25541  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem4  25555  ovolicc2  25557  voliunlem2  25586  voliunlem3  25587  ioombl1lem2  25594  ioombl1lem4  25596  uniioovol  25614  uniiccvol  25615  uniioombllem1  25616  uniioombllem2  25618  uniioombllem3  25620  uniioombllem6  25623  uniioombl  25624  volsup2  25640  vitalilem2  25644  vitalilem4  25646  vitalilem5  25647  mbfsup  25699  mbfinf  25700  mbflimsup  25701  i1fima  25713  i1fima2  25714  itg1cl  25720  itg1ge0  25721  i1fmullem  25729  i1fadd  25730  i1fmul  25731  itg1addlem4  25734  itg1addlem5  25735  i1fmulc  25738  itg1mulc  25739  i1fres  25740  itg10a  25745  itg1ge0a  25746  itg1climres  25749  mbfi1fseqlem4  25753  itg2seq  25777  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2i1fseq2  25791  itg2gt0  25795  itg2cnlem1  25796  itg2cn  25798  dvne0  26050  lhop2  26054  mdegleb  26103  mdegldg  26105  aalioulem3  26376  logccv  26705  efrlim  27012  efrlimOLD  27013  basellem3  27126  fsumvma  27257  lgseisenlem4  27422  noseqind  28298  uhgredgn0  29145  upgredgss  29149  umgredgss  29150  edgupgr  29151  upgredg  29154  usgruspgrb  29200  upgrres1  29330  ubthlem1  30889  minvecolem1  30893  htthlem  30936  ofrn  32649  ofrn2  32650  xppreima2  32661  fsumiunle  32831  ccatws1f1olast  32937  mgcf1o  32993  chnso  33004  gsumhashmul  33064  xrge0tsmsd  33065  symgcom  33103  cycpmcl  33136  cycpmco2lem1  33146  cycpmco2lem5  33150  cycpmco2  33153  cycpmconjv  33162  cycpmconjslem2  33175  elrgspnsubrunlem2  33252  idomsubr  33311  1arithidom  33565  ply1degltdimlem  33673  cmpcref  33849  ordtrestNEW  33920  ordtrest2NEW  33922  xrge0mulc1cn  33940  rge0scvg  33948  esumcst  34064  esumpfinvallem  34075  esumpcvgval  34079  esumiun  34095  omssubadd  34302  carsggect  34320  sibfinima  34341  sitgclg  34344  sitgaddlemb  34350  eulerpartgbij  34374  rrvrnss  34449  orvcval4  34463  erdsze2lem2  35209  cvxpconn  35247  cvxsconn  35248  cvmsss2  35279  cvmliftlem8  35297  cvmlift3lem6  35329  mrsubrn  35518  msubrn  35534  mvtss  35558  mclsssvlem  35567  mclsax  35574  mclsind  35575  neibastop2lem  36361  tailfb  36378  knoppcnlem10  36503  lindsdom  37621  poimirlem2  37629  poimirlem11  37638  poimirlem19  37646  poimirlem27  37654  poimirlem30  37657  mblfinlem2  37665  itg2addnclem2  37679  itg2gt0cn  37682  ftc1anclem3  37702  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anc  37708  cnresima  37771  istotbnd3  37778  sstotbnd2  37781  totbndbnd  37796  prdsbnd  37800  cntotbnd  37803  ismtyima  37810  heibor1lem  37816  heibor  37828  rrnequiv  37842  lsatlss  38997  cdleme50rnlem  40546  sticksstones2  42148  aks6d1c6lem5  42178  cmpfiiin  42708  isnacs3  42721  eldioph2lem2  42772  fnwe2lem2  43063  lmhmfgima  43096  cantnfub2  43335  onnog  43442  gneispacern  44151  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  refsumcn  45035  cncmpmax  45037  elpmrn  45225  climinf  45621  climinf2lem  45721  limsupvaluz2  45753  supcnvlimsup  45755  limsupgtlem  45792  icccncfext  45902  dvsinax  45928  itgsubsticclem  45990  fourierdlem70  46191  fourierdlem82  46203  fge0npnf  46382  sge0resrnlem  46418  sge0isum  46442  sge0seq  46461  meadjiunlem  46480  omeiunle  46532  hoicvr  46563  vonvolmbllem  46675  preimaioomnf  46734  smfco  46817  ackvalsucsucval  48609  aacllem  49320