Theorem frnd 6506

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

Syntax hints:   → wi 4   ⊆ wss 3841  ran crn 5520  ⟶wf 6329

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 400  df-f 6337

This theorem is referenced by:  fliftrel  7068  f1iun  7663  f1dmex  7676  fo2ndf  7836  onoviun  8002  onnseq  8003  smores2  8013  domdifsn  8642  omxpenlem  8660  sucdom2  8669  fodomr  8711  domss2  8719  f1finf1o  8816  f1fi  8877  unirnffid  8882  intrnfi  8946  dffi3  8961  ordtypelem8  9055  ordtypelem9  9056  ordtypelem10  9057  hartogslem1  9072  brwdom2  9103  unxpwdom2  9118  ixpiunwdom  9120  infdifsn  9186  cantnf  9222  ac10ct  9527  numacn  9542  infpwfien  9555  fictb  9738  isf34lem5  9871  isf34lem7  9872  isf34lem6  9873  enfin1ai  9877  canthp1lem2  10146  gch3  10169  wuncval2  10240  peano5nni  11712  hashimarn  13886  hashf1lem1  13899  hashf1lem1OLD  13900  hashf1lem2  13901  ccatrn  14025  swrdrn  14096  pfxrn  14129  cshwrn  14246  limsupgle  14917  limsupgre  14921  isercolllem2  15108  isercoll  15110  isercoll2  15111  climsup  15112  ruclem11  15678  4sqlem11  16384  vdwapf  16401  vdwlem11  16420  0ram  16449  funcres2b  17265  funcres2c  17269  setcepi  17453  yoniso  17644  isacs4lem  17887  mhmima  18098  gsumwspan  18120  frmdss2  18137  cycsubm  18456  cycsubgcl  18460  cycsubgss  18461  ghmrn  18482  conjnmz  18503  cntzmhm  18580  f1omvdconj  18685  odf1o2  18809  pgpssslw  18850  sylow2blem1  18856  lsmssv  18879  smndlsmidm  18892  lsmidmOLD  18900  pj1ghm2  18941  efgsp1  18974  efgrelexlemb  18987  cntzcmnf  19077  cyggenod  19115  gsumval3eu  19136  gsumval3lem2  19138  gsumval3  19139  gsumzsubmcl  19150  gsumzaddlem  19153  gsumzadd  19154  gsumzsplit  19159  gsumconst  19166  gsumzoppg  19176  gsumpt  19194  dmdprdd  19233  dprdfcntz  19249  dprdfeq0  19256  dprdlub  19260  dprdres  19262  dprdss  19263  dprdz  19264  subgdprd  19269  dprd2dlem1  19275  dprd2da  19276  dmdprdsplit2lem  19279  dpjghm2  19298  ablfac1b  19304  lmhmlsp  19933  pj1lmhm2  19985  pjfo  20524  frlmsplit2  20582  frlmsslsp  20605  frlmlbs  20606  frlmup3  20609  frlmup4  20610  lindff1  20629  lindfrn  20630  f1lindf  20631  indlcim  20649  aspval2  20705  mplcoe5lem  20843  mplbas2  20846  mplind  20875  evlslem1  20889  evlseu  20890  gsumply1subr  21002  m2cpmf1  21487  m2cpmghm  21488  iinopn  21646  pptbas  21752  tgrest  21903  resttopon  21905  rest0  21913  restfpw  21923  ordtbaslem  21932  ordtuni  21934  ordtbas2  21935  ordtrest  21946  ordtrest2  21948  cnclsi  22016  cnrest2r  22031  cnprest2  22034  lmss  22042  cncmp  22136  rncmp  22140  discmp  22142  connima  22169  conncn  22170  2ndcdisj  22200  2ndcomap  22202  dis2ndc  22204  lly1stc  22240  comppfsc  22276  kgencmp  22289  1stckgenlem  22297  kgencn3  22302  ptbasfi  22325  txbasval  22350  upxp  22367  uptx  22369  txtube  22384  txcmplem1  22385  txcmplem2  22386  tx1stc  22394  xkoptsub  22398  xkoco2cn  22402  xkococnlem  22403  hmeores  22515  fbasrn  22628  trfilss  22633  trfg  22635  uzrest  22641  rnelfmlem  22696  fclscmpi  22773  alexsublem  22788  ptcmplem1  22796  ptcmplem3  22798  cnextcn  22811  tmdgsum2  22840  subgtgp  22849  subgntr  22851  opnsubg  22852  clsnsg  22854  tgpconncomp  22857  tsmsfbas  22872  prdsdsf  23113  prdsxmetlem  23114  prdsmet  23116  imasdsf1olem  23119  unirnblps  23165  unirnbl  23166  prdsbl  23237  met1stc  23267  met2ndci  23268  prdsxmslem2  23275  xrge0gsumle  23578  xrge0tsms  23579  metdcn2  23584  metdsf  23593  metdsge  23594  cnmptre  23672  bndth  23703  evth  23704  evth2  23705  lebnumlem2  23707  lebnumlem3  23708  reparphti  23742  bcthlem5  24073  minveclem1  24169  minveclem3b  24173  evthicc2  24205  ovolmge0  24222  ovollb  24224  ovolgelb  24225  ovollb2lem  24233  ovollb2  24234  ovolunlem1a  24241  ovolunlem1  24242  ovoliunlem1  24247  ovoliun  24250  ovoliun2  24251  ovolscalem1  24258  ovolicc1  24261  ovolicc2lem4  24265  ovolicc2  24267  voliunlem2  24296  voliunlem3  24297  ioombl1lem2  24304  ioombl1lem4  24306  uniioovol  24324  uniiccvol  24325  uniioombllem1  24326  uniioombllem2  24328  uniioombllem3  24330  uniioombllem6  24333  uniioombl  24334  volsup2  24350  vitalilem2  24354  vitalilem4  24356  vitalilem5  24357  mbfsup  24409  mbfinf  24410  mbflimsup  24411  i1fima  24423  i1fima2  24424  itg1cl  24430  itg1ge0  24431  i1fmullem  24439  i1fadd  24440  i1fmul  24441  itg1addlem4  24444  itg1addlem5  24445  i1fmulc  24448  itg1mulc  24449  i1fres  24450  itg10a  24455  itg1ge0a  24456  itg1climres  24459  mbfi1fseqlem4  24463  itg2seq  24487  itg2monolem1  24495  itg2monolem2  24496  itg2monolem3  24497  itg2mono  24498  itg2i1fseq2  24501  itg2gt0  24505  itg2cnlem1  24506  itg2cn  24508  dvne0  24755  lhop2  24759  mdegleb  24809  mdegldg  24811  aalioulem3  25074  logccv  25398  efrlim  25699  basellem3  25812  fsumvma  25941  lgseisenlem4  26106  uhgredgn0  27065  upgredgss  27069  umgredgss  27070  edgupgr  27071  upgredg  27074  usgruspgrb  27118  upgrres1  27247  ubthlem1  28797  minvecolem1  28801  htthlem  28844  ofrn  30542  ofrn2  30543  xppreima2  30554  fsumiunle  30710  mgcf1o  30850  gsumhashmul  30885  xrge0tsmsd  30886  symgcom  30921  cycpmcl  30952  cycpmco2lem1  30962  cycpmco2lem5  30966  cycpmco2  30969  cycpmconjv  30978  cycpmconjslem2  30991  cmpcref  31364  ordtrestNEW  31435  ordtrest2NEW  31437  xrge0mulc1cn  31455  rge0scvg  31463  esumcst  31593  esumpfinvallem  31604  esumpcvgval  31608  esumiun  31624  omssubadd  31829  carsggect  31847  sibfinima  31868  sitgclg  31871  sitgaddlemb  31877  eulerpartgbij  31901  rrvrnss  31976  orvcval4  31989  erdsze2lem2  32729  cvxpconn  32767  cvxsconn  32768  cvmsss2  32799  cvmliftlem8  32817  cvmlift3lem6  32849  mrsubrn  33038  msubrn  33054  mvtss  33078  mclsssvlem  33087  mclsax  33094  mclsind  33095  neibastop2lem  34179  tailfb  34196  knoppcnlem10  34312  lindsdom  35383  poimirlem2  35391  poimirlem11  35400  poimirlem19  35408  poimirlem27  35416  poimirlem30  35419  mblfinlem2  35427  itg2addnclem2  35441  itg2gt0cn  35444  ftc1anclem3  35464  ftc1anclem6  35467  ftc1anclem7  35468  ftc1anc  35470  cnresima  35534  istotbnd3  35541  sstotbnd2  35544  totbndbnd  35559  prdsbnd  35563  cntotbnd  35566  ismtyima  35573  heibor1lem  35579  heibor  35591  rrnequiv  35605  lsatlss  36622  cdleme50rnlem  38170  sticksstones2  39698  cmpfiiin  40075  isnacs3  40088  eldioph2lem2  40139  fnwe2lem2  40432  lmhmfgima  40465  gneispacern  41278  imo72b2lem0  41306  imo72b2lem2  41308  imo72b2lem1  41310  imo72b2  41314  refsumcn  42095  cncmpmax  42097  elpmrn  42282  climinf  42673  climinf2lem  42773  limsupvaluz2  42805  supcnvlimsup  42807  limsupgtlem  42844  icccncfext  42954  dvsinax  42980  itgsubsticclem  43042  fourierdlem70  43243  fourierdlem82  43255  fge0npnf  43431  sge0resrnlem  43467  sge0isum  43491  sge0seq  43510  meadjiunlem  43529  omeiunle  43581  hoicvr  43612  vonvolmbllem  43724  preimaioomnf  43779  smfco  43859  mgmhmima  44874  ackvalsucsucval  45552  aacllem  45942