Theorem frnd 6659

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

Syntax hints:   → wi 4   ⊆ wss 3897  ran crn 5615  ⟶wf 6477

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 6485

This theorem is referenced by:  f1un  6783  fliftrel  7242  f1iun  7876  f1dmex  7889  fo2ndf  8051  onoviun  8263  onnseq  8264  smores2  8274  domdifsn  8973  omxpenlem  8991  fodomr  9041  domss2  9049  f1domfi  9090  sucdom2  9112  f1finf1o  9157  infn0  9186  f1fi  9198  fodomfir  9212  unirnffid  9231  intrnfi  9300  dffi3  9315  ordtypelem8  9411  ordtypelem9  9412  ordtypelem10  9413  hartogslem1  9428  brwdom2  9459  unxpwdom2  9474  ixpiunwdom  9476  infdifsn  9547  cantnf  9583  ac10ct  9925  numacn  9940  infpwfien  9953  fictb  10135  isf34lem5  10269  isf34lem7  10270  isf34lem6  10271  enfin1ai  10275  canthp1lem2  10544  gch3  10567  wuncval2  10638  peano5nni  12128  hashimarn  14347  hashf1lem1  14362  hashf1lem2  14363  ccatrn  14497  swrdrn  14560  pfxrn  14593  cshwrn  14709  limsupgle  15384  limsupgre  15388  isercolllem2  15573  isercoll  15575  isercoll2  15576  climsup  15577  ruclem11  16149  4sqlem11  16867  vdwapf  16884  vdwlem11  16903  0ram  16932  funcres2b  17804  funcres2c  17810  setcepi  17995  yoniso  18191  isacs4lem  18450  chnso  18530  mgmhmima  18623  mhmima  18733  gsumwspan  18754  frmdss2  18771  cycsubm  19114  cycsubgcl  19118  cycsubgss  19119  ghmrn  19141  conjnmz  19164  ghmqusnsg  19194  ghmquskerlem3  19198  cntzmhm  19253  f1omvdconj  19358  odf1o2  19485  pgpssslw  19526  sylow2blem1  19532  lsmssv  19555  smndlsmidm  19568  pj1ghm2  19616  efgsp1  19649  efgrelexlemb  19662  cntzcmnf  19757  cyggenod  19796  gsumval3eu  19816  gsumval3lem2  19818  gsumval3  19819  gsumzsubmcl  19830  gsumzaddlem  19833  gsumzadd  19834  gsumzsplit  19839  gsumconst  19846  gsumzoppg  19856  gsumpt  19874  dmdprdd  19913  dprdfcntz  19929  dprdfeq0  19936  dprdlub  19940  dprdres  19942  dprdss  19943  dprdz  19944  subgdprd  19949  dprd2dlem1  19955  dprd2da  19956  dmdprdsplit2lem  19959  dpjghm2  19978  ablfac1b  19984  lmhmlsp  20983  pj1lmhm2  21035  pjfo  21652  frlmsplit2  21710  frlmsslsp  21733  frlmlbs  21734  frlmup3  21737  frlmup4  21738  lindff1  21757  lindfrn  21758  f1lindf  21759  indlcim  21777  aspval2  21835  mplcoe5lem  21974  mplbas2  21977  mplind  22005  evlslem1  22017  evlseu  22018  gsumply1subr  22146  m2cpmf1  22658  m2cpmghm  22659  iinopn  22817  pptbas  22923  tgrest  23074  resttopon  23076  rest0  23084  restfpw  23094  ordtbaslem  23103  ordtuni  23105  ordtbas2  23106  ordtrest  23117  ordtrest2  23119  cnclsi  23187  cnrest2r  23202  cnprest2  23205  lmss  23213  cncmp  23307  rncmp  23311  discmp  23313  connima  23340  conncn  23341  2ndcdisj  23371  2ndcomap  23373  dis2ndc  23375  lly1stc  23411  comppfsc  23447  kgencmp  23460  1stckgenlem  23468  kgencn3  23473  ptbasfi  23496  txbasval  23521  upxp  23538  uptx  23540  txtube  23555  txcmplem1  23556  txcmplem2  23557  tx1stc  23565  xkoptsub  23569  xkoco2cn  23573  xkococnlem  23574  hmeores  23686  fbasrn  23799  trfilss  23804  trfg  23806  uzrest  23812  rnelfmlem  23867  fclscmpi  23944  alexsublem  23959  ptcmplem1  23967  ptcmplem3  23969  cnextcn  23982  tmdgsum2  24011  subgtgp  24020  subgntr  24022  opnsubg  24023  clsnsg  24025  tgpconncomp  24028  tsmsfbas  24043  prdsdsf  24282  prdsxmetlem  24283  prdsmet  24285  imasdsf1olem  24288  unirnblps  24334  unirnbl  24335  prdsbl  24406  met1stc  24436  met2ndci  24437  prdsxmslem2  24444  xrge0gsumle  24749  xrge0tsms  24750  metdcn2  24755  metdsf  24764  metdsge  24765  cnmptre  24848  bndth  24884  evth  24885  evth2  24886  lebnumlem2  24888  lebnumlem3  24889  reparphti  24923  reparphtiOLD  24924  bcthlem5  25255  minveclem1  25351  minveclem3b  25355  evthicc2  25388  ovolmge0  25405  ovollb  25407  ovolgelb  25408  ovollb2lem  25416  ovollb2  25417  ovolunlem1a  25424  ovolunlem1  25425  ovoliunlem1  25430  ovoliun  25433  ovoliun2  25434  ovolscalem1  25441  ovolicc1  25444  ovolicc2lem4  25448  ovolicc2  25450  voliunlem2  25479  voliunlem3  25480  ioombl1lem2  25487  ioombl1lem4  25489  uniioovol  25507  uniiccvol  25508  uniioombllem1  25509  uniioombllem2  25511  uniioombllem3  25513  uniioombllem6  25516  uniioombl  25517  volsup2  25533  vitalilem2  25537  vitalilem4  25539  vitalilem5  25540  mbfsup  25592  mbfinf  25593  mbflimsup  25594  i1fima  25606  i1fima2  25607  itg1cl  25613  itg1ge0  25614  i1fmullem  25622  i1fadd  25623  i1fmul  25624  itg1addlem4  25627  itg1addlem5  25628  i1fmulc  25631  itg1mulc  25632  i1fres  25633  itg10a  25638  itg1ge0a  25639  itg1climres  25642  mbfi1fseqlem4  25646  itg2seq  25670  itg2monolem1  25678  itg2monolem2  25679  itg2monolem3  25680  itg2mono  25681  itg2i1fseq2  25684  itg2gt0  25688  itg2cnlem1  25689  itg2cn  25691  dvne0  25943  lhop2  25947  mdegleb  25996  mdegldg  25998  aalioulem3  26269  logccv  26599  efrlim  26906  efrlimOLD  26907  basellem3  27020  fsumvma  27151  lgseisenlem4  27316  noseqind  28222  uhgredgn0  29106  upgredgss  29110  umgredgss  29111  edgupgr  29112  upgredg  29115  usgruspgrb  29161  upgrres1  29291  ubthlem1  30850  minvecolem1  30854  htthlem  30897  ofrn  32621  ofrn2  32622  xppreima2  32633  fsumiunle  32812  ccatws1f1olast  32933  mgcf1o  32984  gsumhashmul  33041  xrge0tsmsd  33042  symgcom  33052  cycpmcl  33085  cycpmco2lem1  33095  cycpmco2lem5  33099  cycpmco2  33102  cycpmconjv  33111  cycpmconjslem2  33124  elrgspnsubrunlem2  33215  idomsubr  33275  1arithidom  33502  psrbasfsupp  33572  esplyfv  33591  ply1degltdimlem  33635  cmpcref  33863  ordtrestNEW  33934  ordtrest2NEW  33936  xrge0mulc1cn  33954  rge0scvg  33962  esumcst  34076  esumpfinvallem  34087  esumpcvgval  34091  esumiun  34107  omssubadd  34313  carsggect  34331  sibfinima  34352  sitgclg  34355  sitgaddlemb  34361  eulerpartgbij  34385  rrvrnss  34460  orvcval4  34474  erdsze2lem2  35248  cvxpconn  35286  cvxsconn  35287  cvmsss2  35318  cvmliftlem8  35336  cvmlift3lem6  35368  mrsubrn  35557  msubrn  35573  mvtss  35597  mclsssvlem  35606  mclsax  35613  mclsind  35614  neibastop2lem  36404  tailfb  36421  knoppcnlem10  36546  lindsdom  37664  poimirlem2  37672  poimirlem11  37681  poimirlem19  37689  poimirlem27  37697  poimirlem30  37700  mblfinlem2  37708  itg2addnclem2  37722  itg2gt0cn  37725  ftc1anclem3  37745  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anc  37751  cnresima  37814  istotbnd3  37821  sstotbnd2  37824  totbndbnd  37839  prdsbnd  37843  cntotbnd  37846  ismtyima  37853  heibor1lem  37859  heibor  37871  rrnequiv  37885  lsatlss  39105  cdleme50rnlem  40653  sticksstones2  42250  aks6d1c6lem5  42280  cmpfiiin  42800  isnacs3  42813  eldioph2lem2  42864  fnwe2lem2  43154  lmhmfgima  43187  cantnfub2  43425  onnog  43532  gneispacern  44241  imo72b2lem2  44270  imo72b2lem1  44272  imo72b2  44275  refsumcn  45137  cncmpmax  45139  elpmrn  45327  climinf  45716  climinf2lem  45814  limsupvaluz2  45846  supcnvlimsup  45848  limsupgtlem  45885  icccncfext  45995  dvsinax  46021  itgsubsticclem  46083  fourierdlem70  46284  fourierdlem82  46296  fge0npnf  46475  sge0resrnlem  46511  sge0isum  46535  sge0seq  46554  meadjiunlem  46573  omeiunle  46625  hoicvr  46656  vonvolmbllem  46768  preimaioomnf  46827  smfco  46910  chnsubseqwl  46987  ackvalsucsucval  48799  aacllem  49912