Theorem frnd 6494

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

Syntax hints:   → wi 4   ⊆ wss 3881  ran crn 5520  ⟶wf 6320

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 6328

This theorem is referenced by:  fliftrel  7040  f1iun  7627  f1dmex  7640  fo2ndf  7800  onoviun  7963  onnseq  7964  smores2  7974  domdifsn  8583  omxpenlem  8601  sucdom2  8610  fodomr  8652  domss2  8660  f1finf1o  8729  f1fi  8795  unirnffid  8800  intrnfi  8864  dffi3  8879  ordtypelem8  8973  ordtypelem9  8974  ordtypelem10  8975  hartogslem1  8990  brwdom2  9021  unxpwdom2  9036  ixpiunwdom  9038  infdifsn  9104  cantnf  9140  ac10ct  9445  numacn  9460  infpwfien  9473  fictb  9656  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  enfin1ai  9795  canthp1lem2  10064  gch3  10087  wuncval2  10158  peano5nni  11628  hashimarn  13797  hashf1lem1  13809  hashf1lem2  13810  ccatrn  13934  swrdrn  14005  pfxrn  14038  cshwrn  14155  limsupgle  14826  limsupgre  14830  isercolllem2  15014  isercoll  15016  isercoll2  15017  climsup  15018  ruclem11  15585  4sqlem11  16281  vdwapf  16298  vdwlem11  16317  0ram  16346  funcres2b  17159  funcres2c  17163  setcepi  17340  yoniso  17527  isacs4lem  17770  mhmima  17981  gsumwspan  18003  frmdss2  18020  cycsubm  18337  cycsubgcl  18341  cycsubgss  18342  ghmrn  18363  conjnmz  18384  cntzmhm  18461  f1omvdconj  18566  odf1o2  18690  pgpssslw  18731  sylow2blem1  18737  lsmssv  18760  smndlsmidm  18773  lsmidmOLD  18781  pj1ghm2  18822  efgsp1  18855  efgrelexlemb  18868  cntzcmnf  18958  cyggenod  18996  gsumval3eu  19017  gsumval3lem2  19019  gsumval3  19020  gsumzsubmcl  19031  gsumzaddlem  19034  gsumzadd  19035  gsumzsplit  19040  gsumconst  19047  gsumzoppg  19057  gsumpt  19075  dmdprdd  19114  dprdfcntz  19130  dprdfeq0  19137  dprdlub  19141  dprdres  19143  dprdss  19144  dprdz  19145  subgdprd  19150  dprd2dlem1  19156  dprd2da  19157  dmdprdsplit2lem  19160  dpjghm2  19179  ablfac1b  19185  lmhmlsp  19814  pj1lmhm2  19866  pjfo  20404  frlmsplit2  20462  frlmsslsp  20485  frlmlbs  20486  frlmup3  20489  frlmup4  20490  lindff1  20509  lindfrn  20510  f1lindf  20511  indlcim  20529  aspval2  20584  mplcoe5lem  20707  mplbas2  20710  mplind  20741  evlslem1  20754  evlseu  20755  gsumply1subr  20863  m2cpmf1  21348  m2cpmghm  21349  iinopn  21507  pptbas  21613  tgrest  21764  resttopon  21766  rest0  21774  restfpw  21784  ordtbaslem  21793  ordtuni  21795  ordtbas2  21796  ordtrest  21807  ordtrest2  21809  cnclsi  21877  cnrest2r  21892  cnprest2  21895  lmss  21903  cncmp  21997  rncmp  22001  discmp  22003  connima  22030  conncn  22031  2ndcdisj  22061  2ndcomap  22063  dis2ndc  22065  lly1stc  22101  comppfsc  22137  kgencmp  22150  1stckgenlem  22158  kgencn3  22163  ptbasfi  22186  txbasval  22211  upxp  22228  uptx  22230  txtube  22245  txcmplem1  22246  txcmplem2  22247  tx1stc  22255  xkoptsub  22259  xkoco2cn  22263  xkococnlem  22264  hmeores  22376  fbasrn  22489  trfilss  22494  trfg  22496  uzrest  22502  rnelfmlem  22557  fclscmpi  22634  alexsublem  22649  ptcmplem1  22657  ptcmplem3  22659  cnextcn  22672  tmdgsum2  22701  subgtgp  22710  subgntr  22712  opnsubg  22713  clsnsg  22715  tgpconncomp  22718  tsmsfbas  22733  prdsdsf  22974  prdsxmetlem  22975  prdsmet  22977  imasdsf1olem  22980  unirnblps  23026  unirnbl  23027  prdsbl  23098  met1stc  23128  met2ndci  23129  prdsxmslem2  23136  xrge0gsumle  23438  xrge0tsms  23439  metdcn2  23444  metdsf  23453  metdsge  23454  cnmptre  23532  bndth  23563  evth  23564  evth2  23565  lebnumlem2  23567  lebnumlem3  23568  reparphti  23602  bcthlem5  23932  minveclem1  24028  minveclem3b  24032  evthicc2  24064  ovolmge0  24081  ovollb  24083  ovolgelb  24084  ovollb2lem  24092  ovollb2  24093  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliun  24109  ovoliun2  24110  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem4  24124  ovolicc2  24126  voliunlem2  24155  voliunlem3  24156  ioombl1lem2  24163  ioombl1lem4  24165  uniioovol  24183  uniiccvol  24184  uniioombllem1  24185  uniioombllem2  24187  uniioombllem3  24189  uniioombllem6  24192  uniioombl  24193  volsup2  24209  vitalilem2  24213  vitalilem4  24215  vitalilem5  24216  mbfsup  24268  mbfinf  24269  mbflimsup  24270  i1fima  24282  i1fima2  24283  itg1cl  24289  itg1ge0  24290  i1fmullem  24298  i1fadd  24299  i1fmul  24300  itg1addlem4  24303  itg1addlem5  24304  i1fmulc  24307  itg1mulc  24308  i1fres  24309  itg10a  24314  itg1ge0a  24315  itg1climres  24318  mbfi1fseqlem4  24322  itg2seq  24346  itg2monolem1  24354  itg2monolem2  24355  itg2monolem3  24356  itg2mono  24357  itg2i1fseq2  24360  itg2gt0  24364  itg2cnlem1  24365  itg2cn  24367  dvne0  24614  lhop2  24618  mdegleb  24665  mdegldg  24667  aalioulem3  24930  logccv  25254  efrlim  25555  basellem3  25668  fsumvma  25797  lgseisenlem4  25962  uhgredgn0  26921  upgredgss  26925  umgredgss  26926  edgupgr  26927  upgredg  26930  usgruspgrb  26974  upgrres1  27103  ubthlem1  28653  minvecolem1  28657  htthlem  28700  ofrn  30400  ofrn2  30401  xppreima2  30413  fsumiunle  30571  gsumhashmul  30741  xrge0tsmsd  30742  symgcom  30777  cycpmcl  30808  cycpmco2lem1  30818  cycpmco2lem5  30822  cycpmco2  30825  cycpmconjv  30834  cycpmconjslem2  30847  cmpcref  31203  ordtrestNEW  31274  ordtrest2NEW  31276  xrge0mulc1cn  31294  rge0scvg  31302  esumcst  31432  esumpfinvallem  31443  esumpcvgval  31447  esumiun  31463  omssubadd  31668  carsggect  31686  sibfinima  31707  sitgclg  31710  sitgaddlemb  31716  eulerpartgbij  31740  rrvrnss  31815  orvcval4  31828  erdsze2lem2  32564  cvxpconn  32602  cvxsconn  32603  cvmsss2  32634  cvmliftlem8  32652  cvmlift3lem6  32684  mrsubrn  32873  msubrn  32889  mvtss  32913  mclsssvlem  32922  mclsax  32929  mclsind  32930  neibastop2lem  33821  tailfb  33838  knoppcnlem10  33954  lindsdom  35051  poimirlem2  35059  poimirlem11  35068  poimirlem19  35076  poimirlem27  35084  poimirlem30  35087  mblfinlem2  35095  itg2addnclem2  35109  itg2gt0cn  35112  ftc1anclem3  35132  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anc  35138  cnresima  35202  istotbnd3  35209  sstotbnd2  35212  totbndbnd  35227  prdsbnd  35231  cntotbnd  35234  ismtyima  35241  heibor1lem  35247  heibor  35259  rrnequiv  35273  lsatlss  36292  cdleme50rnlem  37840  cmpfiiin  39638  isnacs3  39651  eldioph2lem2  39702  fnwe2lem2  39995  lmhmfgima  40028  gneispacern  40841  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2lem1  40874  imo72b2  40878  refsumcn  41659  cncmpmax  41661  elpmrn  41851  climinf  42248  climinf2lem  42348  limsupvaluz2  42380  supcnvlimsup  42382  limsupgtlem  42419  icccncfext  42529  dvsinax  42555  itgsubsticclem  42617  fourierdlem70  42818  fourierdlem82  42830  fge0npnf  43006  sge0resrnlem  43042  sge0isum  43066  sge0seq  43085  meadjiunlem  43104  omeiunle  43156  hoicvr  43187  vonvolmbllem  43299  preimaioomnf  43354  smfco  43434  mgmhmima  44422  ackvalsucsucval  45102  aacllem  45329