Theorem frnd 6712

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

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

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 6537

This theorem is used by:  f1un  6839  fliftrel  7310  f1iun  7942  f1dmex  7955  fo2ndf  8119  onoviun  8333  onnseq  8334  smores2  8344  domdifsn  9059  omxpenlem  9077  fodomr  9127  domss2  9135  f1domfi  9176  sucdom2  9198  f1finf1o  9244  infn0  9273  f1fi  9285  fodomfir  9298  unirnffid  9315  intrnfi  9387  dffi3  9402  ordtypelem8  9498  ordtypelem9  9499  ordtypelem10  9500  hartogslem1  9515  brwdom2  9546  unxpwdom2  9561  ixpiunwdom  9563  infdifsn  9637  cantnf  9673  numacn  10053  infpwfien  10066  fictb  10247  isf34lem5  10381  isf34lem7  10382  isf34lem6  10383  enfin1ai  10387  canthp1lem2  10663  gch3  10686  wuncval2  10757  peano5nni  12261  hashimarn  14506  hashf1lem1  14521  hashf1lem2  14522  ccatrn  14656  swrdrn  14722  pfxrn  14756  cshwrn  14874  limsupgle  15565  limsupgre  15569  isercolllem2  15754  isercoll  15756  isercoll2  15757  climsup  15758  ruclem11  16329  4sqlem11  17048  vdwapf  17065  vdwlem11  17084  0ram  17113  funcres2b  17987  funcres2c  17993  setcepi  18178  yoniso  18374  isacs4lem  18633  chnso  18713  mgmhmima  18818  mhmima  18935  gsumwspan  18956  frmdss2  18973  cycsubm  19331  cycsubgcl  19335  cycsubgss  19336  ghmrn  19357  conjnmz  19380  ghmqusnsg  19410  ghmquskerlem3  19414  cntzmhm  19469  f1omvdconj  19574  odf1o2  19701  pgpssslw  19742  sylow2blem1  19748  lsmssv  19771  smndlsmidm  19784  pj1ghm2  19832  efgsp1  19865  efgrelexlemb  19878  cntzcmnf  19973  cyggenod  20012  gsumval3eu  20032  gsumval3lem2  20034  gsumval3  20035  gsumzsubmcl  20046  gsumzaddlem  20049  gsumzadd  20050  gsumzsplit  20055  gsumconst  20062  gsumzoppg  20072  gsumpt  20090  dmdprdd  20129  dprdfcntz  20145  dprdfeq0  20152  dprdlub  20156  dprdres  20158  dprdss  20159  dprdz  20160  subgdprd  20165  dprd2dlem1  20171  dprd2da  20172  dmdprdsplit2lem  20175  dpjghm2  20194  ablfac1b  20200  lmhmlsp  21234  pj1lmhm2  21286  pjfo  21929  frlmsplit2  21987  frlmsslsp  22010  frlmlbs  22011  frlmup3  22014  frlmup4  22015  lindff1  22034  lindfrn  22035  f1lindf  22036  indlcim  22054  lindsdom  22064  aspval2  22114  mplcoe5lem  22256  mplbas2  22259  mplind  22287  evlslem1  22299  evlseu  22300  gsumply1subr  22459  m2cpmf1  22969  m2cpmghm  22970  iinopn  23128  pptbas  23234  tgrest  23385  resttopon  23387  rest0  23395  restfpw  23405  ordtbaslem  23414  ordtuni  23416  ordtbas2  23417  ordtrest  23428  ordtrest2  23430  cnclsi  23498  cnrest2r  23513  cnprest2  23516  lmss  23524  cncmp  23618  rncmp  23622  discmp  23624  connima  23651  conncn  23652  2ndcdisj  23683  2ndcomap  23685  dis2ndc  23687  lly1stc  23723  comppfsc  23759  kgencmp  23772  1stckgenlem  23780  kgencn3  23785  ptbasfi  23808  txbasval  23833  upxp  23850  uptx  23852  txtube  23867  txcmplem1  23868  txcmplem2  23869  tx1stc  23877  xkoptsub  23881  xkoco2cn  23885  xkococnlem  23886  hmeores  23998  fbasrn  24111  trfilss  24116  trfg  24118  uzrest  24124  rnelfmlem  24179  fclscmpi  24256  alexsublem  24271  ptcmplem1  24279  ptcmplem3  24281  cnextcn  24294  tmdgsum2  24323  subgtgp  24332  subgntr  24334  opnsubg  24335  clsnsg  24337  tgpconncomp  24340  tsmsfbas  24355  prdsdsf  24594  prdsxmetlem  24595  prdsmet  24597  imasdsf1olem  24600  unirnblps  24646  unirnbl  24647  prdsbl  24718  met1stc  24748  met2ndci  24749  prdsxmslem2  24756  xrge0gsumle  25061  xrge0tsms  25062  metdcn2  25067  metdsf  25076  metdsge  25077  cnmptre  25156  bndth  25187  evth  25188  evth2  25189  lebnumlem2  25191  lebnumlem3  25192  reparphti  25226  bcthlem5  25557  minveclem1  25653  minveclem3b  25657  evthicc2  25689  ovolmge0  25706  ovollb  25708  ovolgelb  25709  ovollb2lem  25717  ovollb2  25718  ovolunlem1a  25725  ovolunlem1  25726  ovoliunlem1  25731  ovoliun  25734  ovoliun2  25735  ovolscalem1  25742  ovolicc1  25745  ovolicc2lem4  25749  ovolicc2  25751  voliunlem2  25780  voliunlem3  25781  ioombl1lem2  25788  ioombl1lem4  25790  uniioovol  25808  uniiccvol  25809  uniioombllem1  25810  uniioombllem2  25812  uniioombllem3  25814  uniioombllem6  25817  uniioombl  25818  volsup2  25834  vitalilem2  25838  vitalilem4  25840  vitalilem5  25841  mbfsup  25893  mbfinf  25894  mbflimsup  25895  i1fima  25907  i1fima2  25908  itg1cl  25914  itg1ge0  25915  i1fmullem  25923  i1fadd  25924  i1fmul  25925  itg1addlem4  25928  itg1addlem5  25929  i1fmulc  25932  itg1mulc  25933  i1fres  25934  itg10a  25939  itg1ge0a  25940  itg1climres  25943  mbfi1fseqlem4  25947  itg2seq  25971  itg2monolem1  25979  itg2monolem2  25980  itg2monolem3  25981  itg2mono  25982  itg2i1fseq2  25985  itg2gt0  25989  itg2cnlem1  25990  itg2cn  25992  dvne0  26239  lhop2  26243  mdegleb  26290  mdegldg  26292  rnplynfin  26540  plyconz  26541  aalioulem3  26571  logccv  26901  efrlim  27207  basellem3  27320  fsumvma  27450  lgseisenlem4  27615  noseqind  28558  uhgredgn0  29586  upgredgss  29590  umgredgss  29591  edgupgr  29592  upgredg  29595  usgruspgrb  29644  upgrres1  29774  ubthlem1  31352  minvecolem1  31356  htthlem  31399  ofrn  33113  ofrn2  33114  xppreima2  33125  fsumiunle  33300  ccatws1f1olast  33395  mgcf1o  33444  gsumhashmul  33508  xrge0tsmsd  33514  symgcom  33524  cycpmcl  33557  cycpmco2lem1  33567  cycpmco2lem5  33571  cycpmco2  33574  cycpmconjv  33583  cycpmconjslem2  33596  elrgspnsubrunlem2  33689  idomsubr  33751  1arithidom  33948  psrbasfsupp  34022  esplyfv  34081  esplyfval3  34083  ply1degltdimlem  34133  cmpcref  34361  ordtrestNEW  34432  ordtrest2NEW  34434  xrge0mulc1cn  34452  rge0scvg  34460  esumcst  34574  esumpfinvallem  34585  esumpcvgval  34589  esumiun  34605  omssubadd  34812  carsggect  34830  sibfinima  34851  sitgclg  34854  sitgaddlemb  34860  eulerpartgbij  34884  rrvrnss  34959  orvcval4  34973  erdsze2lem2  35784  cvxpconn  35822  cvxsconn  35823  cvmsss2  35854  cvmliftlem8  35872  cvmlift3lem6  35904  mrsubrn  36093  msubrn  36109  mvtss  36133  mclsssvlem  36142  mclsax  36149  mclsind  36150  neibastop2lem  36980  tailfb  36997  knoppcnlem10  37200  poimirlem2  38372  poimirlem11  38381  poimirlem19  38389  poimirlem27  38397  poimirlem30  38400  mblfinlem2  38408  itg2addnclem2  38422  itg2gt0cn  38425  ftc1anclem3  38445  ftc1anclem6  38448  ftc1anclem7  38449  ftc1anc  38451  cnresima  38515  istotbnd3  38522  sstotbnd2  38525  totbndbnd  38540  prdsbnd  38544  cntotbnd  38547  ismtyima  38554  heibor1lem  38560  heibor  38572  rrnequiv  38586  lsatlss  39870  cdleme50rnlem  41418  sticksstones2  43014  aks6d1c6lem5  43044  cmpfiiin  43543  isnacs3  43556  eldioph2lem2  43607  fnwe2lem2  43893  lmhmfgima  43926  cantnfub2  44164  onnoxpg  44270  gneispacern  44979  imo72b2lem2  45008  imo72b2lem1  45010  imo72b2  45013  refsumcn  45865  cncmpmax  45867  elpmrn  46051  climinf  46437  climinf2lem  46535  limsupvaluz2  46567  supcnvlimsup  46569  limsupgtlem  46606  icccncfext  46716  dvsinax  46742  itgsubsticclem  46804  fourierdlem70  47005  fourierdlem82  47017  fourierdlem113  47048  fge0npnf  47196  sge0resrnlem  47232  sge0isum  47256  sge0seq  47275  meadjiunlem  47294  omeiunle  47346  hoicvr  47377  vonvolmbllem  47489  preimaioomnf  47548  smfco  47631  chnsubseqwl  47708  tmachlem-fssscan  47779  ackvalsucsucval  49619  aacllem  50773