Theorem frnd 6718

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ran crn 5652  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6542

This theorem is used by:  f1un  6845  fliftrel  7316  f1iun  7956  f1dmex  7969  fo2ndf  8132  onoviun  8351  onnseq  8352  smores2  8362  domdifsn  9079  omxpenlem  9097  fodomr  9147  domss2  9155  f1domfi  9196  sucdom2  9218  f1finf1o  9264  infn0  9294  f1fi  9306  fodomfir  9319  unirnffid  9336  intrnfi  9408  dffi3  9423  ordtypelem8  9519  ordtypelem9  9520  ordtypelem10  9521  hartogslem1  9536  brwdom2  9567  unxpwdom2  9582  ixpiunwdom  9584  infdifsn  9658  cantnf  9694  numacn  10128  infpwfien  10141  fictb  10322  isf34lem5  10456  isf34lem7  10457  isf34lem6  10458  enfin1ai  10462  canthp1lem2  10738  gch3  10761  wuncval2  10832  peano5nni  12338  hashimarn  14585  hashf1lem1  14600  hashf1lem2  14601  ccatrn  14735  swrdrn  14801  pfxrn  14835  cshwrn  14953  limsupgle  15644  limsupgre  15648  isercolllem2  15833  isercoll  15835  isercoll2  15836  climsup  15837  ruclem11  16408  4sqlem11  17133  vdwapf  17150  vdwlem11  17169  0ram  17198  funcres2b  18072  funcres2c  18078  setcepi  18263  yoniso  18459  isacs4lem  18718  chnso  18798  mgmhmima  18904  mhmima  19021  gsumwspan  19042  frmdss2  19059  cycsubm  19417  cycsubgcl  19421  cycsubgss  19422  ghmrn  19443  conjnmz  19466  ghmqusnsg  19496  ghmquskerlem3  19500  cntzmhm  19555  f1omvdconj  19660  odf1o2  19787  pgpssslw  19828  sylow2blem1  19834  lsmssv  19857  smndlsmidm  19870  pj1ghm2  19918  efgsp1  19951  efgrelexlemb  19964  cntzcmnf  20059  cyggenod  20098  gsumval3eu  20118  gsumval3lem2  20120  gsumval3  20121  gsumzsubmcl  20132  gsumzaddlem  20135  gsumzadd  20136  gsumzsplit  20141  gsumconst  20148  gsumzoppg  20158  gsumpt  20176  dmdprdd  20215  dprdfcntz  20231  dprdfeq0  20238  dprdlub  20242  dprdres  20244  dprdss  20245  dprdz  20246  subgdprd  20251  dprd2dlem1  20257  dprd2da  20258  dmdprdsplit2lem  20261  dpjghm2  20280  ablfac1b  20286  lmhmlsp  21324  pj1lmhm2  21376  pjfo  22021  frlmsplit2  22079  frlmsslsp  22102  frlmlbs  22103  frlmup3  22106  frlmup4  22107  lindff1  22126  lindfrn  22127  f1lindf  22128  indlcim  22146  lindsdom  22156  aspval2  22206  mplcoe5lem  22348  mplbas2  22351  mplind  22379  evlslem1  22391  evlseu  22392  gsumply1subr  22551  m2cpmf1  23061  m2cpmghm  23062  iinopn  23220  pptbas  23326  tgrest  23477  resttopon  23479  rest0  23487  restfpw  23497  ordtbaslem  23506  ordtuni  23508  ordtbas2  23509  ordtrest  23520  ordtrest2  23522  cnclsi  23590  cnrest2r  23605  cnprest2  23608  lmss  23616  cncmp  23710  rncmp  23714  discmp  23716  connima  23743  conncn  23744  2ndcdisj  23775  2ndcomap  23777  dis2ndc  23779  lly1stc  23815  comppfsc  23851  kgencmp  23864  1stckgenlem  23872  kgencn3  23877  ptbasfi  23900  txbasval  23925  upxp  23942  uptx  23944  txtube  23959  txcmplem1  23960  txcmplem2  23961  tx1stc  23969  xkoptsub  23973  xkoco2cn  23977  xkococnlem  23978  hmeores  24090  fbasrn  24203  trfilss  24208  trfg  24210  uzrest  24216  rnelfmlem  24271  fclscmpi  24348  alexsublem  24363  ptcmplem1  24371  ptcmplem3  24373  cnextcn  24386  tmdgsum2  24415  subgtgp  24424  subgntr  24426  opnsubg  24427  clsnsg  24429  tgpconncomp  24432  tsmsfbas  24447  prdsdsf  24686  prdsxmetlem  24687  prdsmet  24689  imasdsf1olem  24692  unirnblps  24738  unirnbl  24739  prdsbl  24810  met1stc  24840  met2ndci  24841  prdsxmslem2  24848  xrge0gsumle  25153  xrge0tsms  25154  metdcn2  25159  metdsf  25168  metdsge  25169  cnmptre  25248  bndth  25279  evth  25280  evth2  25281  lebnumlem2  25283  lebnumlem3  25284  reparphti  25318  bcthlem5  25649  minveclem1  25745  minveclem3b  25749  evthicc2  25781  ovolmge0  25798  ovollb  25800  ovolgelb  25801  ovollb2lem  25809  ovollb2  25810  ovolunlem1a  25817  ovolunlem1  25818  ovoliunlem1  25823  ovoliun  25826  ovoliun2  25827  ovolscalem1  25834  ovolicc1  25837  ovolicc2lem4  25841  ovolicc2  25843  voliunlem2  25872  voliunlem3  25873  ioombl1lem2  25880  ioombl1lem4  25882  uniioovol  25900  uniiccvol  25901  uniioombllem1  25902  uniioombllem2  25904  uniioombllem3  25906  uniioombllem6  25909  uniioombl  25910  volsup2  25926  vitalilem2  25930  vitalilem4  25932  vitalilem5  25933  mbfsup  25985  mbfinf  25986  mbflimsup  25987  i1fima  25999  i1fima2  26000  itg1cl  26006  itg1ge0  26007  i1fmullem  26015  i1fadd  26016  i1fmul  26017  itg1addlem4  26020  itg1addlem5  26021  i1fmulc  26024  itg1mulc  26025  i1fres  26026  itg10a  26031  itg1ge0a  26032  itg1climres  26035  mbfi1fseqlem4  26039  itg2seq  26063  itg2monolem1  26071  itg2monolem2  26072  itg2monolem3  26073  itg2mono  26074  itg2i1fseq2  26077  itg2gt0  26081  itg2cnlem1  26082  itg2cn  26084  dvne0  26331  lhop2  26335  mdegleb  26382  mdegldg  26384  rnplynfin  26630  plyconz  26631  aalioulem3  26661  logccv  26991  efrlim  27297  basellem3  27410  fsumvma  27540  lgseisenlem4  27705  noseqind  28678  uhgredgn0  29706  upgredgss  29710  umgredgss  29711  edgupgr  29712  upgredg  29715  usgruspgrb  29764  upgrres1  29894  ubthlem1  31472  minvecolem1  31476  htthlem  31519  ofrn  33233  ofrn2  33234  xppreima2  33245  fsumiunle  33420  ccatws1f1olast  33515  mgcf1o  33564  gsumhashmul  33628  xrge0tsmsd  33634  symgcom  33644  cycpmcl  33677  cycpmco2lem1  33687  cycpmco2lem5  33691  cycpmco2  33694  cycpmconjv  33703  cycpmconjslem2  33716  elrgspnsubrunlem2  33809  idomsubr  33871  1arithidom  34069  psrbasfsupp  34143  esplyfv  34202  esplyfval3  34204  ply1degltdimlem  34254  cmpcref  34482  ordtrestNEW  34553  ordtrest2NEW  34555  xrge0mulc1cn  34573  rge0scvg  34581  esumcst  34695  esumpfinvallem  34706  esumpcvgval  34710  esumiun  34726  omssubadd  34932  carsggect  34950  sibfinima  34971  sitgclg  34974  sitgaddlemb  34980  eulerpartgbij  35004  rrvrnss  35079  orvcval4  35093  onprcf1acwevd  35897  erdsze2lem2  35969  cvxpconn  36007  cvxsconn  36008  cvmsss2  36039  cvmliftlem8  36057  cvmlift3lem6  36089  mrsubrn  36278  msubrn  36294  mvtss  36318  mclsssvlem  36327  mclsax  36334  mclsind  36335  neibastop2lem  37148  tailfb  37165  knoppcnlem10  37368  poimirlem2  38540  poimirlem11  38549  poimirlem19  38557  poimirlem27  38565  poimirlem30  38568  mblfinlem2  38576  itg2addnclem2  38590  itg2gt0cn  38593  ftc1anclem3  38613  ftc1anclem6  38616  ftc1anclem7  38617  ftc1anc  38619  cnresima  38698  istotbnd3  38705  sstotbnd2  38708  totbndbnd  38723  prdsbnd  38727  cntotbnd  38730  ismtyima  38737  heibor1lem  38743  heibor  38755  rrnequiv  38769  lsatlss  40053  cdleme50rnlem  41601  sticksstones2  43197  aks6d1c6lem5  43227  cmpfiiin  43707  isnacs3  43720  eldioph2lem2  43771  lmhmfgima  44085  cantnfub2  44323  onnoxpg  44429  gneispacern  45137  imo72b2lem2  45166  imo72b2lem1  45168  imo72b2  45171  refsumcn  46046  cncmpmax  46048  elpmrn  46232  climinf  46617  climinf2lem  46715  limsupvaluz2  46747  supcnvlimsup  46749  limsupgtlem  46786  icccncfext  46896  dvsinax  46922  itgsubsticclem  46984  fourierdlem70  47185  fourierdlem82  47197  fourierdlem113  47228  fge0npnf  47376  sge0resrnlem  47412  sge0isum  47436  sge0seq  47455  meadjiunlem  47474  omeiunle  47526  hoicvr  47557  vonvolmbllem  47669  preimaioomnf  47728  smfco  47811  chnsubseqwl  47888  tmachlem-fssscan  47959  ackvalsucsucval  49799  aacllem  50938