Theorem frnd 6726

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

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

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 6550

This theorem is used by:  f1un  6853  fliftrel  7323  f1iun  7963  f1dmex  7976  fo2ndf  8142  onoviun  8362  onnseq  8363  smores2  8373  domdifsn  9090  omxpenlem  9108  fodomr  9158  domss2  9166  f1domfi  9207  sucdom2  9229  f1finf1o  9275  infn0  9305  f1fi  9317  fodomfir  9330  unirnffid  9347  intrnfi  9418  dffi3  9433  ordtypelem8  9529  ordtypelem9  9530  ordtypelem10  9531  hartogslem1  9546  brwdom2  9577  unxpwdom2  9592  ixpiunwdom  9594  infdifsn  9668  cantnf  9704  numacn  10138  infpwfien  10151  fictb  10332  isf34lem5  10466  isf34lem7  10467  isf34lem6  10468  enfin1ai  10472  canthp1lem2  10748  gch3  10771  wuncval2  10842  peano5nni  12348  hashimarn  14595  hashf1lem1  14610  hashf1lem2  14611  ccatrn  14745  swrdrn  14812  pfxrn  14846  cshwrn  14964  limsupgle  15656  limsupgre  15660  isercolllem2  15845  isercoll  15847  isercoll2  15848  climsup  15849  ruclem11  16420  4sqlem11  17145  vdwapf  17162  vdwlem11  17181  0ram  17210  funcres2b  18084  funcres2c  18090  setcepi  18275  yoniso  18471  isacs4lem  18730  chnso  18810  mgmhmima  18916  mhmima  19033  gsumwspan  19054  frmdss2  19071  cycsubm  19429  cycsubgcl  19433  cycsubgss  19434  ghmrn  19455  conjnmz  19478  ghmqusnsg  19508  ghmquskerlem3  19512  cntzmhm  19567  f1omvdconj  19672  odf1o2  19799  pgpssslw  19840  sylow2blem1  19846  lsmssv  19869  smndlsmidm  19882  pj1ghm2  19930  efgsp1  19963  efgrelexlemb  19976  cntzcmnf  20071  cyggenod  20110  gsumval3eu  20130  gsumval3lem2  20132  gsumval3  20133  gsumzsubmcl  20144  gsumzaddlem  20147  gsumzadd  20148  gsumzsplit  20153  gsumconst  20160  gsumzoppg  20170  gsumpt  20188  dmdprdd  20227  dprdfcntz  20243  dprdfeq0  20250  dprdlub  20254  dprdres  20256  dprdss  20257  dprdz  20258  subgdprd  20263  dprd2dlem1  20269  dprd2da  20270  dmdprdsplit2lem  20273  dpjghm2  20292  ablfac1b  20298  lmhmlsp  21336  pj1lmhm2  21388  pjfo  22033  frlmsplit2  22091  frlmsslsp  22114  frlmlbs  22115  frlmup3  22118  frlmup4  22119  lindff1  22138  lindfrn  22139  f1lindf  22140  indlcim  22158  lindsdom  22168  aspval2  22218  mplcoe5lem  22360  mplbas2  22363  mplind  22391  evlslem1  22403  evlseu  22404  gsumply1subr  22563  m2cpmf1  23073  m2cpmghm  23074  iinopn  23232  pptbas  23338  tgrest  23489  resttopon  23491  rest0  23499  restfpw  23509  ordtbaslem  23518  ordtuni  23520  ordtbas2  23521  ordtrest  23532  ordtrest2  23534  cnclsi  23602  cnrest2r  23617  cnprest2  23620  lmss  23628  cncmp  23722  rncmp  23726  discmp  23728  connima  23755  conncn  23756  2ndcdisj  23787  2ndcomap  23789  dis2ndc  23791  lly1stc  23827  comppfsc  23863  kgencmp  23876  1stckgenlem  23884  kgencn3  23889  ptbasfi  23912  txbasval  23937  upxp  23954  uptx  23956  txtube  23971  txcmplem1  23972  txcmplem2  23973  tx1stc  23981  xkoptsub  23985  xkoco2cn  23989  xkococnlem  23990  hmeores  24102  fbasrn  24215  trfilss  24220  trfg  24222  uzrest  24228  rnelfmlem  24283  fclscmpi  24360  alexsublem  24375  ptcmplem1  24383  ptcmplem3  24385  cnextcn  24398  tmdgsum2  24427  subgtgp  24436  subgntr  24438  opnsubg  24439  clsnsg  24441  tgpconncomp  24444  tsmsfbas  24459  prdsdsf  24698  prdsxmetlem  24699  prdsmet  24701  imasdsf1olem  24704  unirnblps  24750  unirnbl  24751  prdsbl  24822  met1stc  24852  met2ndci  24853  prdsxmslem2  24860  xrge0gsumle  25165  xrge0tsms  25166  metdcn2  25171  metdsf  25180  metdsge  25181  cnmptre  25260  bndth  25291  evth  25292  evth2  25293  lebnumlem2  25295  lebnumlem3  25296  reparphti  25330  bcthlem5  25661  minveclem1  25757  minveclem3b  25761  evthicc2  25793  ovolmge0  25810  ovollb  25812  ovolgelb  25813  ovollb2lem  25821  ovollb2  25822  ovolunlem1a  25829  ovolunlem1  25830  ovoliunlem1  25835  ovoliun  25838  ovoliun2  25839  ovolscalem1  25846  ovolicc1  25849  ovolicc2lem4  25853  ovolicc2  25855  voliunlem2  25884  voliunlem3  25885  ioombl1lem2  25892  ioombl1lem4  25894  uniioovol  25912  uniiccvol  25913  uniioombllem1  25914  uniioombllem2  25916  uniioombllem3  25918  uniioombllem6  25921  uniioombl  25922  volsup2  25938  vitalilem2  25942  vitalilem4  25944  vitalilem5  25945  mbfsup  25997  mbfinf  25998  mbflimsup  25999  i1fima  26011  i1fima2  26012  itg1cl  26018  itg1ge0  26019  i1fmullem  26027  i1fadd  26028  i1fmul  26029  itg1addlem4  26032  itg1addlem5  26033  i1fmulc  26036  itg1mulc  26037  i1fres  26038  itg10a  26043  itg1ge0a  26044  itg1climres  26047  mbfi1fseqlem4  26051  itg2seq  26075  itg2monolem1  26083  itg2monolem2  26084  itg2monolem3  26085  itg2mono  26086  itg2i1fseq2  26089  itg2gt0  26093  itg2cnlem1  26094  itg2cn  26096  dvne0  26343  lhop2  26347  mdegleb  26394  mdegldg  26396  rnplynfin  26642  plyconz  26643  aalioulem3  26673  logccv  27003  efrlim  27309  basellem3  27422  fsumvma  27552  lgseisenlem4  27717  noseqind  28690  uhgredgn0  29718  upgredgss  29722  umgredgss  29723  edgupgr  29724  upgredg  29727  usgruspgrb  29776  upgrres1  29906  ubthlem1  31484  minvecolem1  31488  htthlem  31531  ofrn  33287  ofrn2  33288  xppreima2  33299  fsumiunle  33473  ccatws1f1olast  33568  mgcf1o  33617  gsumhashmul  33681  xrge0tsmsd  33687  symgcom  33697  cycpmcl  33730  cycpmco2lem1  33740  cycpmco2lem5  33744  cycpmco2  33747  cycpmconjv  33756  cycpmconjslem2  33769  elrgspnsubrunlem2  33862  idomsubr  33924  1arithidom  34122  psrbasfsupp  34196  esplyfv  34255  esplyfval3  34257  ply1degltdimlem  34307  cmpcref  34535  ordtrestNEW  34606  ordtrest2NEW  34608  xrge0mulc1cn  34626  rge0scvg  34634  esumcst  34748  esumpfinvallem  34759  esumpcvgval  34763  esumiun  34779  omssubadd  34985  carsggect  35003  sibfinima  35024  sitgclg  35027  sitgaddlemb  35033  eulerpartgbij  35057  rrvrnss  35132  orvcval4  35146  onf1we  35780  onprcf1acwevd  36001  erdsze2lem2  36090  cvxpconn  36128  cvxsconn  36129  cvmsss2  36160  cvmliftlem8  36178  cvmlift3lem6  36210  mrsubrn  36399  msubrn  36415  mvtss  36439  mclsssvlem  36448  mclsax  36455  mclsind  36456  neibastop2lem  37275  tailfb  37292  knoppcnlem10  37495  pibt2  38480  poimirlem2  38680  poimirlem11  38689  poimirlem19  38697  poimirlem27  38705  poimirlem30  38708  mblfinlem2  38716  itg2addnclem2  38730  itg2gt0cn  38733  ftc1anclem3  38753  ftc1anclem6  38756  ftc1anclem7  38757  ftc1anc  38759  cnresima  38838  istotbnd3  38845  sstotbnd2  38848  totbndbnd  38863  prdsbnd  38867  cntotbnd  38870  ismtyima  38877  heibor1lem  38883  heibor  38895  rrnequiv  38909  lsatlss  40193  cdleme50rnlem  41741  sticksstones2  43337  aks6d1c6lem5  43367  cmpfiiin  43848  isnacs3  43861  eldioph2lem2  43912  lmhmfgima  44226  cantnfub2  44464  onnoxpg  44570  gneispacern  45278  imo72b2lem2  45307  imo72b2lem1  45309  imo72b2  45312  refsumcn  46186  cncmpmax  46188  elpmrn  46372  climinf  46757  climinf2lem  46855  limsupvaluz2  46887  supcnvlimsup  46889  limsupgtlem  46926  icccncfext  47036  dvsinax  47062  itgsubsticclem  47124  fourierdlem70  47325  fourierdlem82  47337  fourierdlem113  47368  fge0npnf  47516  sge0resrnlem  47552  sge0isum  47576  sge0seq  47595  meadjiunlem  47614  omeiunle  47666  hoicvr  47697  vonvolmbllem  47809  preimaioomnf  47868  smfco  47951  chnsubseqwl  48028  tmachlem-fssscan  48099  ackvalsucsucval  49939  aacllem  51153