Theorem frnd 6699

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

Syntax hints:   → wi 4   ⊆ wss 3917  ran crn 5642  ⟶wf 6510

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 6518

This theorem is referenced by:  f1un  6823  fliftrel  7286  f1iun  7925  f1dmex  7938  fo2ndf  8103  onoviun  8315  onnseq  8316  smores2  8326  domdifsn  9028  omxpenlem  9047  sucdom2OLD  9056  fodomr  9098  domss2  9106  f1domfi  9151  sucdom2  9173  f1finf1o  9223  f1finf1oOLD  9224  infn0  9258  f1fi  9270  fodomfir  9286  unirnffid  9305  intrnfi  9374  dffi3  9389  ordtypelem8  9485  ordtypelem9  9486  ordtypelem10  9487  hartogslem1  9502  brwdom2  9533  unxpwdom2  9548  ixpiunwdom  9550  infdifsn  9617  cantnf  9653  ac10ct  9994  numacn  10009  infpwfien  10022  fictb  10204  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  enfin1ai  10344  canthp1lem2  10613  gch3  10636  wuncval2  10707  peano5nni  12196  hashimarn  14412  hashf1lem1  14427  hashf1lem2  14428  ccatrn  14561  swrdrn  14624  pfxrn  14657  cshwrn  14774  limsupgle  15450  limsupgre  15454  isercolllem2  15639  isercoll  15641  isercoll2  15642  climsup  15643  ruclem11  16215  4sqlem11  16933  vdwapf  16950  vdwlem11  16969  0ram  16998  funcres2b  17866  funcres2c  17872  setcepi  18057  yoniso  18253  isacs4lem  18510  mgmhmima  18649  mhmima  18759  gsumwspan  18780  frmdss2  18797  cycsubm  19141  cycsubgcl  19145  cycsubgss  19146  ghmrn  19168  conjnmz  19191  ghmqusnsg  19221  ghmquskerlem3  19225  cntzmhm  19280  f1omvdconj  19383  odf1o2  19510  pgpssslw  19551  sylow2blem1  19557  lsmssv  19580  smndlsmidm  19593  pj1ghm2  19641  efgsp1  19674  efgrelexlemb  19687  cntzcmnf  19782  cyggenod  19821  gsumval3eu  19841  gsumval3lem2  19843  gsumval3  19844  gsumzsubmcl  19855  gsumzaddlem  19858  gsumzadd  19859  gsumzsplit  19864  gsumconst  19871  gsumzoppg  19881  gsumpt  19899  dmdprdd  19938  dprdfcntz  19954  dprdfeq0  19961  dprdlub  19965  dprdres  19967  dprdss  19968  dprdz  19969  subgdprd  19974  dprd2dlem1  19980  dprd2da  19981  dmdprdsplit2lem  19984  dpjghm2  20003  ablfac1b  20009  lmhmlsp  20963  pj1lmhm2  21015  pjfo  21631  frlmsplit2  21689  frlmsslsp  21712  frlmlbs  21713  frlmup3  21716  frlmup4  21717  lindff1  21736  lindfrn  21737  f1lindf  21738  indlcim  21756  aspval2  21814  mplcoe5lem  21953  mplbas2  21956  mplind  21984  evlslem1  21996  evlseu  21997  gsumply1subr  22125  m2cpmf1  22637  m2cpmghm  22638  iinopn  22796  pptbas  22902  tgrest  23053  resttopon  23055  rest0  23063  restfpw  23073  ordtbaslem  23082  ordtuni  23084  ordtbas2  23085  ordtrest  23096  ordtrest2  23098  cnclsi  23166  cnrest2r  23181  cnprest2  23184  lmss  23192  cncmp  23286  rncmp  23290  discmp  23292  connima  23319  conncn  23320  2ndcdisj  23350  2ndcomap  23352  dis2ndc  23354  lly1stc  23390  comppfsc  23426  kgencmp  23439  1stckgenlem  23447  kgencn3  23452  ptbasfi  23475  txbasval  23500  upxp  23517  uptx  23519  txtube  23534  txcmplem1  23535  txcmplem2  23536  tx1stc  23544  xkoptsub  23548  xkoco2cn  23552  xkococnlem  23553  hmeores  23665  fbasrn  23778  trfilss  23783  trfg  23785  uzrest  23791  rnelfmlem  23846  fclscmpi  23923  alexsublem  23938  ptcmplem1  23946  ptcmplem3  23948  cnextcn  23961  tmdgsum2  23990  subgtgp  23999  subgntr  24001  opnsubg  24002  clsnsg  24004  tgpconncomp  24007  tsmsfbas  24022  prdsdsf  24262  prdsxmetlem  24263  prdsmet  24265  imasdsf1olem  24268  unirnblps  24314  unirnbl  24315  prdsbl  24386  met1stc  24416  met2ndci  24417  prdsxmslem2  24424  xrge0gsumle  24729  xrge0tsms  24730  metdcn2  24735  metdsf  24744  metdsge  24745  cnmptre  24828  bndth  24864  evth  24865  evth2  24866  lebnumlem2  24868  lebnumlem3  24869  reparphti  24903  reparphtiOLD  24904  bcthlem5  25235  minveclem1  25331  minveclem3b  25335  evthicc2  25368  ovolmge0  25385  ovollb  25387  ovolgelb  25388  ovollb2lem  25396  ovollb2  25397  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliun  25413  ovoliun2  25414  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem4  25428  ovolicc2  25430  voliunlem2  25459  voliunlem3  25460  ioombl1lem2  25467  ioombl1lem4  25469  uniioovol  25487  uniiccvol  25488  uniioombllem1  25489  uniioombllem2  25491  uniioombllem3  25493  uniioombllem6  25496  uniioombl  25497  volsup2  25513  vitalilem2  25517  vitalilem4  25519  vitalilem5  25520  mbfsup  25572  mbfinf  25573  mbflimsup  25574  i1fima  25586  i1fima2  25587  itg1cl  25593  itg1ge0  25594  i1fmullem  25602  i1fadd  25603  i1fmul  25604  itg1addlem4  25607  itg1addlem5  25608  i1fmulc  25611  itg1mulc  25612  i1fres  25613  itg10a  25618  itg1ge0a  25619  itg1climres  25622  mbfi1fseqlem4  25626  itg2seq  25650  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2i1fseq2  25664  itg2gt0  25668  itg2cnlem1  25669  itg2cn  25671  dvne0  25923  lhop2  25927  mdegleb  25976  mdegldg  25978  aalioulem3  26249  logccv  26579  efrlim  26886  efrlimOLD  26887  basellem3  27000  fsumvma  27131  lgseisenlem4  27296  noseqind  28193  uhgredgn0  29062  upgredgss  29066  umgredgss  29067  edgupgr  29068  upgredg  29071  usgruspgrb  29117  upgrres1  29247  ubthlem1  30806  minvecolem1  30810  htthlem  30853  ofrn  32570  ofrn2  32571  xppreima2  32582  fsumiunle  32761  ccatws1f1olast  32881  mgcf1o  32936  chnso  32947  gsumhashmul  33008  xrge0tsmsd  33009  symgcom  33047  cycpmcl  33080  cycpmco2lem1  33090  cycpmco2lem5  33094  cycpmco2  33097  cycpmconjv  33106  cycpmconjslem2  33119  elrgspnsubrunlem2  33206  idomsubr  33266  1arithidom  33515  ply1degltdimlem  33625  cmpcref  33847  ordtrestNEW  33918  ordtrest2NEW  33920  xrge0mulc1cn  33938  rge0scvg  33946  esumcst  34060  esumpfinvallem  34071  esumpcvgval  34075  esumiun  34091  omssubadd  34298  carsggect  34316  sibfinima  34337  sitgclg  34340  sitgaddlemb  34346  eulerpartgbij  34370  rrvrnss  34445  orvcval4  34459  erdsze2lem2  35198  cvxpconn  35236  cvxsconn  35237  cvmsss2  35268  cvmliftlem8  35286  cvmlift3lem6  35318  mrsubrn  35507  msubrn  35523  mvtss  35547  mclsssvlem  35556  mclsax  35563  mclsind  35564  neibastop2lem  36355  tailfb  36372  knoppcnlem10  36497  lindsdom  37615  poimirlem2  37623  poimirlem11  37632  poimirlem19  37640  poimirlem27  37648  poimirlem30  37651  mblfinlem2  37659  itg2addnclem2  37673  itg2gt0cn  37676  ftc1anclem3  37696  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anc  37702  cnresima  37765  istotbnd3  37772  sstotbnd2  37775  totbndbnd  37790  prdsbnd  37794  cntotbnd  37797  ismtyima  37804  heibor1lem  37810  heibor  37822  rrnequiv  37836  lsatlss  38996  cdleme50rnlem  40545  sticksstones2  42142  aks6d1c6lem5  42172  cmpfiiin  42692  isnacs3  42705  eldioph2lem2  42756  fnwe2lem2  43047  lmhmfgima  43080  cantnfub2  43318  onnog  43425  gneispacern  44134  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  refsumcn  45031  cncmpmax  45033  elpmrn  45221  climinf  45611  climinf2lem  45711  limsupvaluz2  45743  supcnvlimsup  45745  limsupgtlem  45782  icccncfext  45892  dvsinax  45918  itgsubsticclem  45980  fourierdlem70  46181  fourierdlem82  46193  fge0npnf  46372  sge0resrnlem  46408  sge0isum  46432  sge0seq  46451  meadjiunlem  46470  omeiunle  46522  hoicvr  46553  vonvolmbllem  46665  preimaioomnf  46724  smfco  46807  ackvalsucsucval  48681  aacllem  49794