Theorem frnd 6725

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

Syntax hints:   → wi 4   ⊆ wss 3948  ran crn 5677  ⟶wf 6539

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 206  df-an 396  df-f 6547

This theorem is referenced by:  f1un  6853  fliftrel  7308  f1iun  7934  f1dmex  7947  fo2ndf  8112  onoviun  8349  onnseq  8350  smores2  8360  domdifsn  9060  omxpenlem  9079  sucdom2OLD  9088  fodomr  9134  domss2  9142  f1domfi  9190  sucdom2  9212  f1finf1o  9277  f1finf1oOLD  9278  infn0  9313  f1fi  9345  unirnffid  9350  intrnfi  9417  dffi3  9432  ordtypelem8  9526  ordtypelem9  9527  ordtypelem10  9528  hartogslem1  9543  brwdom2  9574  unxpwdom2  9589  ixpiunwdom  9591  infdifsn  9658  cantnf  9694  ac10ct  10035  numacn  10050  infpwfien  10063  fictb  10246  isf34lem5  10379  isf34lem7  10380  isf34lem6  10381  enfin1ai  10385  canthp1lem2  10654  gch3  10677  wuncval2  10748  peano5nni  12222  hashimarn  14407  hashf1lem1  14422  hashf1lem1OLD  14423  hashf1lem2  14424  ccatrn  14546  swrdrn  14609  pfxrn  14642  cshwrn  14759  limsupgle  15428  limsupgre  15432  isercolllem2  15619  isercoll  15621  isercoll2  15622  climsup  15623  ruclem11  16190  4sqlem11  16895  vdwapf  16912  vdwlem11  16931  0ram  16960  funcres2b  17854  funcres2c  17859  setcepi  18045  yoniso  18245  isacs4lem  18504  mgmhmima  18643  mhmima  18745  gsumwspan  18766  frmdss2  18783  cycsubm  19121  cycsubgcl  19125  cycsubgss  19126  ghmrn  19147  conjnmz  19170  cntzmhm  19250  f1omvdconj  19359  odf1o2  19486  pgpssslw  19527  sylow2blem1  19533  lsmssv  19556  smndlsmidm  19569  pj1ghm2  19617  efgsp1  19650  efgrelexlemb  19663  cntzcmnf  19758  cyggenod  19797  gsumval3eu  19817  gsumval3lem2  19819  gsumval3  19820  gsumzsubmcl  19831  gsumzaddlem  19834  gsumzadd  19835  gsumzsplit  19840  gsumconst  19847  gsumzoppg  19857  gsumpt  19875  dmdprdd  19914  dprdfcntz  19930  dprdfeq0  19937  dprdlub  19941  dprdres  19943  dprdss  19944  dprdz  19945  subgdprd  19950  dprd2dlem1  19956  dprd2da  19957  dmdprdsplit2lem  19960  dpjghm2  19979  ablfac1b  19985  lmhmlsp  20808  pj1lmhm2  20860  pjfo  21493  frlmsplit2  21551  frlmsslsp  21574  frlmlbs  21575  frlmup3  21578  frlmup4  21579  lindff1  21598  lindfrn  21599  f1lindf  21600  indlcim  21618  aspval2  21675  mplcoe5lem  21818  mplbas2  21821  mplind  21855  evlslem1  21869  evlseu  21870  gsumply1subr  21989  m2cpmf1  22478  m2cpmghm  22479  iinopn  22637  pptbas  22744  tgrest  22896  resttopon  22898  rest0  22906  restfpw  22916  ordtbaslem  22925  ordtuni  22927  ordtbas2  22928  ordtrest  22939  ordtrest2  22941  cnclsi  23009  cnrest2r  23024  cnprest2  23027  lmss  23035  cncmp  23129  rncmp  23133  discmp  23135  connima  23162  conncn  23163  2ndcdisj  23193  2ndcomap  23195  dis2ndc  23197  lly1stc  23233  comppfsc  23269  kgencmp  23282  1stckgenlem  23290  kgencn3  23295  ptbasfi  23318  txbasval  23343  upxp  23360  uptx  23362  txtube  23377  txcmplem1  23378  txcmplem2  23379  tx1stc  23387  xkoptsub  23391  xkoco2cn  23395  xkococnlem  23396  hmeores  23508  fbasrn  23621  trfilss  23626  trfg  23628  uzrest  23634  rnelfmlem  23689  fclscmpi  23766  alexsublem  23781  ptcmplem1  23789  ptcmplem3  23791  cnextcn  23804  tmdgsum2  23833  subgtgp  23842  subgntr  23844  opnsubg  23845  clsnsg  23847  tgpconncomp  23850  tsmsfbas  23865  prdsdsf  24106  prdsxmetlem  24107  prdsmet  24109  imasdsf1olem  24112  unirnblps  24158  unirnbl  24159  prdsbl  24233  met1stc  24263  met2ndci  24264  prdsxmslem2  24271  xrge0gsumle  24582  xrge0tsms  24583  metdcn2  24588  metdsf  24597  metdsge  24598  cnmptre  24681  bndth  24717  evth  24718  evth2  24719  lebnumlem2  24721  lebnumlem3  24722  reparphti  24756  reparphtiOLD  24757  bcthlem5  25089  minveclem1  25185  minveclem3b  25189  evthicc2  25222  ovolmge0  25239  ovollb  25241  ovolgelb  25242  ovollb2lem  25250  ovollb2  25251  ovolunlem1a  25258  ovolunlem1  25259  ovoliunlem1  25264  ovoliun  25267  ovoliun2  25268  ovolscalem1  25275  ovolicc1  25278  ovolicc2lem4  25282  ovolicc2  25284  voliunlem2  25313  voliunlem3  25314  ioombl1lem2  25321  ioombl1lem4  25323  uniioovol  25341  uniiccvol  25342  uniioombllem1  25343  uniioombllem2  25345  uniioombllem3  25347  uniioombllem6  25350  uniioombl  25351  volsup2  25367  vitalilem2  25371  vitalilem4  25373  vitalilem5  25374  mbfsup  25426  mbfinf  25427  mbflimsup  25428  i1fima  25440  i1fima2  25441  itg1cl  25447  itg1ge0  25448  i1fmullem  25456  i1fadd  25457  i1fmul  25458  itg1addlem4  25461  itg1addlem4OLD  25462  itg1addlem5  25463  i1fmulc  25466  itg1mulc  25467  i1fres  25468  itg10a  25473  itg1ge0a  25474  itg1climres  25477  mbfi1fseqlem4  25481  itg2seq  25505  itg2monolem1  25513  itg2monolem2  25514  itg2monolem3  25515  itg2mono  25516  itg2i1fseq2  25519  itg2gt0  25523  itg2cnlem1  25524  itg2cn  25526  dvne0  25777  lhop2  25781  mdegleb  25831  mdegldg  25833  aalioulem3  26097  logccv  26422  efrlim  26725  basellem3  26838  fsumvma  26967  lgseisenlem4  27132  peano5n0s  27950  uhgredgn0  28670  upgredgss  28674  umgredgss  28675  edgupgr  28676  upgredg  28679  usgruspgrb  28723  upgrres1  28852  ubthlem1  30405  minvecolem1  30409  htthlem  30452  ofrn  32146  ofrn2  32147  xppreima2  32158  fsumiunle  32317  mgcf1o  32455  gsumhashmul  32493  xrge0tsmsd  32494  symgcom  32529  cycpmcl  32560  cycpmco2lem1  32570  cycpmco2lem5  32574  cycpmco2  32577  cycpmconjv  32586  cycpmconjslem2  32599  ghmquskerlem3  32820  ply1degltdimlem  33010  cmpcref  33143  ordtrestNEW  33214  ordtrest2NEW  33216  xrge0mulc1cn  33234  rge0scvg  33242  esumcst  33374  esumpfinvallem  33385  esumpcvgval  33389  esumiun  33405  omssubadd  33612  carsggect  33630  sibfinima  33651  sitgclg  33654  sitgaddlemb  33660  eulerpartgbij  33684  rrvrnss  33759  orvcval4  33772  erdsze2lem2  34508  cvxpconn  34546  cvxsconn  34547  cvmsss2  34578  cvmliftlem8  34596  cvmlift3lem6  34628  mrsubrn  34817  msubrn  34833  mvtss  34857  mclsssvlem  34866  mclsax  34873  mclsind  34874  neibastop2lem  35561  tailfb  35578  knoppcnlem10  35694  lindsdom  36798  poimirlem2  36806  poimirlem11  36815  poimirlem19  36823  poimirlem27  36831  poimirlem30  36834  mblfinlem2  36842  itg2addnclem2  36856  itg2gt0cn  36859  ftc1anclem3  36879  ftc1anclem6  36882  ftc1anclem7  36883  ftc1anc  36885  cnresima  36948  istotbnd3  36955  sstotbnd2  36958  totbndbnd  36973  prdsbnd  36977  cntotbnd  36980  ismtyima  36987  heibor1lem  36993  heibor  37005  rrnequiv  37019  lsatlss  38182  cdleme50rnlem  39731  sticksstones2  41282  cmpfiiin  41750  isnacs3  41763  eldioph2lem2  41814  fnwe2lem2  42108  lmhmfgima  42141  cantnfub2  42387  onnog  42495  gneispacern  43204  imo72b2lem0  43232  imo72b2lem2  43234  imo72b2lem1  43236  imo72b2  43239  refsumcn  44029  cncmpmax  44031  elpmrn  44230  climinf  44633  climinf2lem  44733  limsupvaluz2  44765  supcnvlimsup  44767  limsupgtlem  44804  icccncfext  44914  dvsinax  44940  itgsubsticclem  45002  fourierdlem70  45203  fourierdlem82  45215  fge0npnf  45394  sge0resrnlem  45430  sge0isum  45454  sge0seq  45473  meadjiunlem  45492  omeiunle  45544  hoicvr  45575  vonvolmbllem  45687  preimaioomnf  45746  smfco  45829  ackvalsucsucval  47474  aacllem  47948