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 3962  ran crn 5689  ⟶wf 6558

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 6566

This theorem is referenced by:  f1un  6868  fliftrel  7327  f1iun  7966  f1dmex  7979  fo2ndf  8144  onoviun  8381  onnseq  8382  smores2  8392  domdifsn  9092  omxpenlem  9111  sucdom2OLD  9120  fodomr  9166  domss2  9174  f1domfi  9218  sucdom2  9240  f1finf1o  9302  f1finf1oOLD  9303  infn0  9337  f1fi  9349  fodomfir  9365  unirnffid  9384  intrnfi  9453  dffi3  9468  ordtypelem8  9562  ordtypelem9  9563  ordtypelem10  9564  hartogslem1  9579  brwdom2  9610  unxpwdom2  9625  ixpiunwdom  9627  infdifsn  9694  cantnf  9730  ac10ct  10071  numacn  10086  infpwfien  10099  fictb  10281  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  enfin1ai  10421  canthp1lem2  10690  gch3  10713  wuncval2  10784  peano5nni  12266  hashimarn  14475  hashf1lem1  14490  hashf1lem2  14491  ccatrn  14623  swrdrn  14686  pfxrn  14719  cshwrn  14836  limsupgle  15509  limsupgre  15513  isercolllem2  15698  isercoll  15700  isercoll2  15701  climsup  15702  ruclem11  16272  4sqlem11  16988  vdwapf  17005  vdwlem11  17024  0ram  17053  funcres2b  17947  funcres2c  17954  setcepi  18141  yoniso  18341  isacs4lem  18601  mgmhmima  18740  mhmima  18850  gsumwspan  18871  frmdss2  18888  cycsubm  19232  cycsubgcl  19236  cycsubgss  19237  ghmrn  19259  conjnmz  19282  ghmqusnsg  19312  ghmquskerlem3  19316  cntzmhm  19371  f1omvdconj  19478  odf1o2  19605  pgpssslw  19646  sylow2blem1  19652  lsmssv  19675  smndlsmidm  19688  pj1ghm2  19736  efgsp1  19769  efgrelexlemb  19782  cntzcmnf  19877  cyggenod  19916  gsumval3eu  19936  gsumval3lem2  19938  gsumval3  19939  gsumzsubmcl  19950  gsumzaddlem  19953  gsumzadd  19954  gsumzsplit  19959  gsumconst  19966  gsumzoppg  19976  gsumpt  19994  dmdprdd  20033  dprdfcntz  20049  dprdfeq0  20056  dprdlub  20060  dprdres  20062  dprdss  20063  dprdz  20064  subgdprd  20069  dprd2dlem1  20075  dprd2da  20076  dmdprdsplit2lem  20079  dpjghm2  20098  ablfac1b  20104  lmhmlsp  21065  pj1lmhm2  21117  pjfo  21752  frlmsplit2  21810  frlmsslsp  21833  frlmlbs  21834  frlmup3  21837  frlmup4  21838  lindff1  21857  lindfrn  21858  f1lindf  21859  indlcim  21877  aspval2  21935  mplcoe5lem  22074  mplbas2  22077  mplind  22111  evlslem1  22123  evlseu  22124  gsumply1subr  22250  m2cpmf1  22764  m2cpmghm  22765  iinopn  22923  pptbas  23030  tgrest  23182  resttopon  23184  rest0  23192  restfpw  23202  ordtbaslem  23211  ordtuni  23213  ordtbas2  23214  ordtrest  23225  ordtrest2  23227  cnclsi  23295  cnrest2r  23310  cnprest2  23313  lmss  23321  cncmp  23415  rncmp  23419  discmp  23421  connima  23448  conncn  23449  2ndcdisj  23479  2ndcomap  23481  dis2ndc  23483  lly1stc  23519  comppfsc  23555  kgencmp  23568  1stckgenlem  23576  kgencn3  23581  ptbasfi  23604  txbasval  23629  upxp  23646  uptx  23648  txtube  23663  txcmplem1  23664  txcmplem2  23665  tx1stc  23673  xkoptsub  23677  xkoco2cn  23681  xkococnlem  23682  hmeores  23794  fbasrn  23907  trfilss  23912  trfg  23914  uzrest  23920  rnelfmlem  23975  fclscmpi  24052  alexsublem  24067  ptcmplem1  24075  ptcmplem3  24077  cnextcn  24090  tmdgsum2  24119  subgtgp  24128  subgntr  24130  opnsubg  24131  clsnsg  24133  tgpconncomp  24136  tsmsfbas  24151  prdsdsf  24392  prdsxmetlem  24393  prdsmet  24395  imasdsf1olem  24398  unirnblps  24444  unirnbl  24445  prdsbl  24519  met1stc  24549  met2ndci  24550  prdsxmslem2  24557  xrge0gsumle  24868  xrge0tsms  24869  metdcn2  24874  metdsf  24883  metdsge  24884  cnmptre  24967  bndth  25003  evth  25004  evth2  25005  lebnumlem2  25007  lebnumlem3  25008  reparphti  25042  reparphtiOLD  25043  bcthlem5  25375  minveclem1  25471  minveclem3b  25475  evthicc2  25508  ovolmge0  25525  ovollb  25527  ovolgelb  25528  ovollb2lem  25536  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun  25553  ovoliun2  25554  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem4  25568  ovolicc2  25570  voliunlem2  25599  voliunlem3  25600  ioombl1lem2  25607  ioombl1lem4  25609  uniioovol  25627  uniiccvol  25628  uniioombllem1  25629  uniioombllem2  25631  uniioombllem3  25633  uniioombllem6  25636  uniioombl  25637  volsup2  25653  vitalilem2  25657  vitalilem4  25659  vitalilem5  25660  mbfsup  25712  mbfinf  25713  mbflimsup  25714  i1fima  25726  i1fima2  25727  itg1cl  25733  itg1ge0  25734  i1fmullem  25742  i1fadd  25743  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  i1fmulc  25752  itg1mulc  25753  i1fres  25754  itg10a  25759  itg1ge0a  25760  itg1climres  25763  mbfi1fseqlem4  25767  itg2seq  25791  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2i1fseq2  25805  itg2gt0  25809  itg2cnlem1  25810  itg2cn  25812  dvne0  26064  lhop2  26068  mdegleb  26117  mdegldg  26119  aalioulem3  26390  logccv  26719  efrlim  27026  efrlimOLD  27027  basellem3  27140  fsumvma  27271  lgseisenlem4  27436  noseqind  28312  uhgredgn0  29159  upgredgss  29163  umgredgss  29164  edgupgr  29165  upgredg  29168  usgruspgrb  29214  upgrres1  29344  ubthlem1  30898  minvecolem1  30902  htthlem  30945  ofrn  32655  ofrn2  32656  xppreima2  32667  fsumiunle  32835  ccatws1f1olast  32921  mgcf1o  32977  chnso  32987  gsumhashmul  33046  xrge0tsmsd  33047  symgcom  33085  cycpmcl  33118  cycpmco2lem1  33128  cycpmco2lem5  33132  cycpmco2  33135  cycpmconjv  33144  cycpmconjslem2  33157  idomsubr  33290  1arithidom  33544  ply1degltdimlem  33649  cmpcref  33810  ordtrestNEW  33881  ordtrest2NEW  33883  xrge0mulc1cn  33901  rge0scvg  33909  esumcst  34043  esumpfinvallem  34054  esumpcvgval  34058  esumiun  34074  omssubadd  34281  carsggect  34299  sibfinima  34320  sitgclg  34323  sitgaddlemb  34329  eulerpartgbij  34353  rrvrnss  34428  orvcval4  34441  erdsze2lem2  35188  cvxpconn  35226  cvxsconn  35227  cvmsss2  35258  cvmliftlem8  35276  cvmlift3lem6  35308  mrsubrn  35497  msubrn  35513  mvtss  35537  mclsssvlem  35546  mclsax  35553  mclsind  35554  neibastop2lem  36342  tailfb  36359  knoppcnlem10  36484  lindsdom  37600  poimirlem2  37608  poimirlem11  37617  poimirlem19  37625  poimirlem27  37633  poimirlem30  37636  mblfinlem2  37644  itg2addnclem2  37658  itg2gt0cn  37661  ftc1anclem3  37681  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anc  37687  cnresima  37750  istotbnd3  37757  sstotbnd2  37760  totbndbnd  37775  prdsbnd  37779  cntotbnd  37782  ismtyima  37789  heibor1lem  37795  heibor  37807  rrnequiv  37821  lsatlss  38977  cdleme50rnlem  40526  sticksstones2  42128  aks6d1c6lem5  42158  cmpfiiin  42684  isnacs3  42697  eldioph2lem2  42748  fnwe2lem2  43039  lmhmfgima  43072  cantnfub2  43311  onnog  43418  gneispacern  44127  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  refsumcn  44967  cncmpmax  44969  elpmrn  45162  climinf  45561  climinf2lem  45661  limsupvaluz2  45693  supcnvlimsup  45695  limsupgtlem  45732  icccncfext  45842  dvsinax  45868  itgsubsticclem  45930  fourierdlem70  46131  fourierdlem82  46143  fge0npnf  46322  sge0resrnlem  46358  sge0isum  46382  sge0seq  46401  meadjiunlem  46420  omeiunle  46472  hoicvr  46503  vonvolmbllem  46615  preimaioomnf  46674  smfco  46757  ackvalsucsucval  48537  aacllem  49031