Theorem frnd 6755

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

Syntax hints:   → wi 4   ⊆ wss 3976  ran crn 5701  ⟶wf 6569

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 6577

This theorem is referenced by:  f1un  6882  fliftrel  7344  f1iun  7984  f1dmex  7997  fo2ndf  8162  onoviun  8399  onnseq  8400  smores2  8410  domdifsn  9120  omxpenlem  9139  sucdom2OLD  9148  fodomr  9194  domss2  9202  f1domfi  9247  sucdom2  9269  f1finf1o  9333  f1finf1oOLD  9334  infn0  9368  f1fi  9380  fodomfir  9396  unirnffid  9415  intrnfi  9485  dffi3  9500  ordtypelem8  9594  ordtypelem9  9595  ordtypelem10  9596  hartogslem1  9611  brwdom2  9642  unxpwdom2  9657  ixpiunwdom  9659  infdifsn  9726  cantnf  9762  ac10ct  10103  numacn  10118  infpwfien  10131  fictb  10313  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  enfin1ai  10453  canthp1lem2  10722  gch3  10745  wuncval2  10816  peano5nni  12296  hashimarn  14489  hashf1lem1  14504  hashf1lem2  14505  ccatrn  14637  swrdrn  14700  pfxrn  14733  cshwrn  14850  limsupgle  15523  limsupgre  15527  isercolllem2  15714  isercoll  15716  isercoll2  15717  climsup  15718  ruclem11  16288  4sqlem11  17002  vdwapf  17019  vdwlem11  17038  0ram  17067  funcres2b  17961  funcres2c  17968  setcepi  18155  yoniso  18355  isacs4lem  18614  mgmhmima  18753  mhmima  18860  gsumwspan  18881  frmdss2  18898  cycsubm  19242  cycsubgcl  19246  cycsubgss  19247  ghmrn  19269  conjnmz  19292  ghmqusnsg  19322  ghmquskerlem3  19326  cntzmhm  19381  f1omvdconj  19488  odf1o2  19615  pgpssslw  19656  sylow2blem1  19662  lsmssv  19685  smndlsmidm  19698  pj1ghm2  19746  efgsp1  19779  efgrelexlemb  19792  cntzcmnf  19887  cyggenod  19926  gsumval3eu  19946  gsumval3lem2  19948  gsumval3  19949  gsumzsubmcl  19960  gsumzaddlem  19963  gsumzadd  19964  gsumzsplit  19969  gsumconst  19976  gsumzoppg  19986  gsumpt  20004  dmdprdd  20043  dprdfcntz  20059  dprdfeq0  20066  dprdlub  20070  dprdres  20072  dprdss  20073  dprdz  20074  subgdprd  20079  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  dpjghm2  20108  ablfac1b  20114  lmhmlsp  21071  pj1lmhm2  21123  pjfo  21758  frlmsplit2  21816  frlmsslsp  21839  frlmlbs  21840  frlmup3  21843  frlmup4  21844  lindff1  21863  lindfrn  21864  f1lindf  21865  indlcim  21883  aspval2  21941  mplcoe5lem  22080  mplbas2  22083  mplind  22117  evlslem1  22129  evlseu  22130  gsumply1subr  22256  m2cpmf1  22770  m2cpmghm  22771  iinopn  22929  pptbas  23036  tgrest  23188  resttopon  23190  rest0  23198  restfpw  23208  ordtbaslem  23217  ordtuni  23219  ordtbas2  23220  ordtrest  23231  ordtrest2  23233  cnclsi  23301  cnrest2r  23316  cnprest2  23319  lmss  23327  cncmp  23421  rncmp  23425  discmp  23427  connima  23454  conncn  23455  2ndcdisj  23485  2ndcomap  23487  dis2ndc  23489  lly1stc  23525  comppfsc  23561  kgencmp  23574  1stckgenlem  23582  kgencn3  23587  ptbasfi  23610  txbasval  23635  upxp  23652  uptx  23654  txtube  23669  txcmplem1  23670  txcmplem2  23671  tx1stc  23679  xkoptsub  23683  xkoco2cn  23687  xkococnlem  23688  hmeores  23800  fbasrn  23913  trfilss  23918  trfg  23920  uzrest  23926  rnelfmlem  23981  fclscmpi  24058  alexsublem  24073  ptcmplem1  24081  ptcmplem3  24083  cnextcn  24096  tmdgsum2  24125  subgtgp  24134  subgntr  24136  opnsubg  24137  clsnsg  24139  tgpconncomp  24142  tsmsfbas  24157  prdsdsf  24398  prdsxmetlem  24399  prdsmet  24401  imasdsf1olem  24404  unirnblps  24450  unirnbl  24451  prdsbl  24525  met1stc  24555  met2ndci  24556  prdsxmslem2  24563  xrge0gsumle  24874  xrge0tsms  24875  metdcn2  24880  metdsf  24889  metdsge  24890  cnmptre  24973  bndth  25009  evth  25010  evth2  25011  lebnumlem2  25013  lebnumlem3  25014  reparphti  25048  reparphtiOLD  25049  bcthlem5  25381  minveclem1  25477  minveclem3b  25481  evthicc2  25514  ovolmge0  25531  ovollb  25533  ovolgelb  25534  ovollb2lem  25542  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliun  25559  ovoliun2  25560  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem4  25574  ovolicc2  25576  voliunlem2  25605  voliunlem3  25606  ioombl1lem2  25613  ioombl1lem4  25615  uniioovol  25633  uniiccvol  25634  uniioombllem1  25635  uniioombllem2  25637  uniioombllem3  25639  uniioombllem6  25642  uniioombl  25643  volsup2  25659  vitalilem2  25663  vitalilem4  25665  vitalilem5  25666  mbfsup  25718  mbfinf  25719  mbflimsup  25720  i1fima  25732  i1fima2  25733  itg1cl  25739  itg1ge0  25740  i1fmullem  25748  i1fadd  25749  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  i1fmulc  25758  itg1mulc  25759  i1fres  25760  itg10a  25765  itg1ge0a  25766  itg1climres  25769  mbfi1fseqlem4  25773  itg2seq  25797  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2i1fseq2  25811  itg2gt0  25815  itg2cnlem1  25816  itg2cn  25818  dvne0  26070  lhop2  26074  mdegleb  26123  mdegldg  26125  aalioulem3  26394  logccv  26723  efrlim  27030  efrlimOLD  27031  basellem3  27144  fsumvma  27275  lgseisenlem4  27440  noseqind  28316  uhgredgn0  29163  upgredgss  29167  umgredgss  29168  edgupgr  29169  upgredg  29172  usgruspgrb  29218  upgrres1  29348  ubthlem1  30902  minvecolem1  30906  htthlem  30949  ofrn  32658  ofrn2  32659  xppreima2  32669  fsumiunle  32833  ccatws1f1olast  32919  mgcf1o  32976  chnso  32986  gsumhashmul  33040  xrge0tsmsd  33041  symgcom  33076  cycpmcl  33109  cycpmco2lem1  33119  cycpmco2lem5  33123  cycpmco2  33126  cycpmconjv  33135  cycpmconjslem2  33148  idomsubr  33276  1arithidom  33530  ply1degltdimlem  33635  cmpcref  33796  ordtrestNEW  33867  ordtrest2NEW  33869  xrge0mulc1cn  33887  rge0scvg  33895  esumcst  34027  esumpfinvallem  34038  esumpcvgval  34042  esumiun  34058  omssubadd  34265  carsggect  34283  sibfinima  34304  sitgclg  34307  sitgaddlemb  34313  eulerpartgbij  34337  rrvrnss  34412  orvcval4  34425  erdsze2lem2  35172  cvxpconn  35210  cvxsconn  35211  cvmsss2  35242  cvmliftlem8  35260  cvmlift3lem6  35292  mrsubrn  35481  msubrn  35497  mvtss  35521  mclsssvlem  35530  mclsax  35537  mclsind  35538  neibastop2lem  36326  tailfb  36343  knoppcnlem10  36468  lindsdom  37574  poimirlem2  37582  poimirlem11  37591  poimirlem19  37599  poimirlem27  37607  poimirlem30  37610  mblfinlem2  37618  itg2addnclem2  37632  itg2gt0cn  37635  ftc1anclem3  37655  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anc  37661  cnresima  37724  istotbnd3  37731  sstotbnd2  37734  totbndbnd  37749  prdsbnd  37753  cntotbnd  37756  ismtyima  37763  heibor1lem  37769  heibor  37781  rrnequiv  37795  lsatlss  38952  cdleme50rnlem  40501  sticksstones2  42104  aks6d1c6lem5  42134  cmpfiiin  42653  isnacs3  42666  eldioph2lem2  42717  fnwe2lem2  43008  lmhmfgima  43041  cantnfub2  43284  onnog  43391  gneispacern  44100  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  refsumcn  44930  cncmpmax  44932  elpmrn  45127  climinf  45527  climinf2lem  45627  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  icccncfext  45808  dvsinax  45834  itgsubsticclem  45896  fourierdlem70  46097  fourierdlem82  46109  fge0npnf  46288  sge0resrnlem  46324  sge0isum  46348  sge0seq  46367  meadjiunlem  46386  omeiunle  46438  hoicvr  46469  vonvolmbllem  46581  preimaioomnf  46640  smfco  46723  ackvalsucsucval  48422  aacllem  48895