MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frnd Structured version   Visualization version   GIF version

Theorem frnd 6517
Description: Deduction form of frn 6516. 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
StepHypRef Expression
1 frnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 frn 6516 . 2 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3939  ran crn 5554  wf 6347
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 208  df-an 397  df-f 6355
This theorem is referenced by:  fliftrel  7056  f1iunw  7636  f1iun  7639  f1dmex  7652  fo2ndf  7811  onoviun  7974  onnseq  7975  smores2  7985  domdifsn  8592  omxpenlem  8610  fodomr  8660  domss2  8668  sucdom2  8706  f1finf1o  8737  f1fi  8803  unirnffid  8808  intrnfi  8872  dffi3  8887  ordtypelem8  8981  ordtypelem9  8982  ordtypelem10  8983  hartogslem1  8998  brwdom2  9029  unxpwdom2  9044  ixpiunwdom  9047  infdifsn  9112  cantnf  9148  ac10ct  9452  numacn  9467  infpwfien  9480  fictb  9659  isf34lem5  9792  isf34lem7  9793  isf34lem6  9794  enfin1ai  9798  canthp1lem2  10067  gch3  10090  wuncval2  10161  peano5nni  11633  hashimarn  13794  hashf1lem1  13806  hashf1lem2  13807  ccatrn  13936  swrdrn  14007  pfxrn  14040  cshwrn  14157  limsupgle  14827  limsupgre  14831  isercolllem2  15015  isercoll  15017  isercoll2  15018  climsup  15019  ruclem11  15585  4sqlem11  16283  vdwapf  16300  vdwlem11  16319  0ram  16348  funcres2b  17159  funcres2c  17163  setcepi  17340  yoniso  17527  isacs4lem  17770  mhmima  17974  gsumwspan  17996  frmdss2  18013  cycsubm  18277  cycsubgcl  18281  cycsubgss  18282  ghmrn  18303  conjnmz  18324  cntzmhm  18401  f1omvdconj  18496  odf1o2  18620  pgpssslw  18661  sylow2blem1  18667  lsmssv  18690  smndlsmidm  18703  lsmidmOLD  18711  pj1ghm2  18752  efgsp1  18785  efgrelexlemb  18798  cntzcmnf  18887  cyggenod  18925  gsumval3eu  18946  gsumval3lem2  18948  gsumval3  18949  gsumzsubmcl  18960  gsumzaddlem  18963  gsumzadd  18964  gsumzsplit  18969  gsumconst  18976  gsumzoppg  18986  gsumpt  19004  dmdprdd  19043  dprdfcntz  19059  dprdfeq0  19066  dprdlub  19070  dprdres  19072  dprdss  19073  dprdz  19074  subgdprd  19079  dprd2dlem1  19085  dprd2da  19086  dmdprdsplit2lem  19089  dpjghm2  19108  ablfac1b  19114  lmhmlsp  19743  pj1lmhm2  19795  aspval2  20048  mplcoe5lem  20168  mplbas2  20171  mplind  20202  evlslem1  20215  evlseu  20216  gsumply1subr  20321  pjfo  20777  frlmsplit2  20835  frlmsslsp  20858  frlmlbs  20859  frlmup3  20862  frlmup4  20863  lindff1  20882  lindfrn  20883  f1lindf  20884  indlcim  20902  m2cpmf1  21269  m2cpmghm  21270  iinopn  21428  pptbas  21534  tgrest  21685  resttopon  21687  rest0  21695  restfpw  21705  ordtbaslem  21714  ordtuni  21716  ordtbas2  21717  ordtrest  21728  ordtrest2  21730  cnclsi  21798  cnrest2r  21813  cnprest2  21816  lmss  21824  cncmp  21918  rncmp  21922  discmp  21924  connima  21951  conncn  21952  2ndcdisj  21982  2ndcomap  21984  dis2ndc  21986  lly1stc  22022  comppfsc  22058  kgencmp  22071  1stckgenlem  22079  kgencn3  22084  ptbasfi  22107  txbasval  22132  upxp  22149  uptx  22151  txtube  22166  txcmplem1  22167  txcmplem2  22168  tx1stc  22176  xkoptsub  22180  xkoco2cn  22184  xkococnlem  22185  hmeores  22297  fbasrn  22410  trfilss  22415  trfg  22417  uzrest  22423  rnelfmlem  22478  fclscmpi  22555  alexsublem  22570  ptcmplem1  22578  ptcmplem3  22580  cnextcn  22593  tmdgsum2  22622  subgtgp  22631  subgntr  22632  opnsubg  22633  clsnsg  22635  tgpconncomp  22638  tsmsfbas  22653  prdsdsf  22894  prdsxmetlem  22895  prdsmet  22897  imasdsf1olem  22900  unirnblps  22946  unirnbl  22947  prdsbl  23018  met1stc  23048  met2ndci  23049  prdsxmslem2  23056  xrge0gsumle  23358  xrge0tsms  23359  metdcn2  23364  metdsf  23373  metdsge  23374  cnmptre  23448  bndth  23479  evth  23480  evth2  23481  lebnumlem2  23483  lebnumlem3  23484  reparphti  23518  bcthlem5  23848  minveclem1  23944  minveclem3b  23948  evthicc2  23978  ovolmge0  23995  ovollb  23997  ovolgelb  23998  ovollb2lem  24006  ovollb2  24007  ovolunlem1a  24014  ovolunlem1  24015  ovoliunlem1  24020  ovoliun  24023  ovoliun2  24024  ovolscalem1  24031  ovolicc1  24034  ovolicc2lem4  24038  ovolicc2  24040  voliunlem2  24069  voliunlem3  24070  ioombl1lem2  24077  ioombl1lem4  24079  uniioovol  24097  uniiccvol  24098  uniioombllem1  24099  uniioombllem2  24101  uniioombllem3  24103  uniioombllem6  24106  uniioombl  24107  volsup2  24123  vitalilem2  24127  vitalilem4  24129  vitalilem5  24130  mbfsup  24182  mbfinf  24183  mbflimsup  24184  i1fima  24196  i1fima2  24197  itg1cl  24203  itg1ge0  24204  i1fmullem  24212  i1fadd  24213  i1fmul  24214  itg1addlem4  24217  itg1addlem5  24218  i1fmulc  24221  itg1mulc  24222  i1fres  24223  itg10a  24228  itg1ge0a  24229  itg1climres  24232  mbfi1fseqlem4  24236  itg2seq  24260  itg2monolem1  24268  itg2monolem2  24269  itg2monolem3  24270  itg2mono  24271  itg2i1fseq2  24274  itg2gt0  24278  itg2cnlem1  24279  itg2cn  24281  dvne0  24525  lhop2  24529  mdegleb  24575  mdegldg  24577  aalioulem3  24840  logccv  25161  efrlim  25463  basellem3  25576  fsumvma  25705  lgseisenlem4  25870  uhgredgn0  26829  upgredgss  26833  umgredgss  26834  edgupgr  26835  upgredg  26838  usgruspgrb  26882  upgrres1  27011  ubthlem1  28563  minvecolem1  28567  htthlem  28610  ofrn  30303  ofrn2  30304  xppreima2  30312  fsumiunle  30461  xrge0tsmsd  30608  symgcom  30643  cycpmcl  30674  cycpmco2lem1  30684  cycpmco2lem5  30688  cycpmco2  30691  cycpmconjv  30700  cycpmconjslem2  30713  cmpcref  31002  ordtrestNEW  31052  ordtrest2NEW  31054  xrge0mulc1cn  31072  rge0scvg  31080  esumcst  31210  esumpfinvallem  31221  esumpcvgval  31225  esumiun  31241  omssubadd  31446  carsggect  31464  sibfinima  31485  sitgclg  31488  sitgaddlemb  31494  eulerpartgbij  31518  rrvrnss  31593  orvcval4  31606  erdsze2lem2  32337  cvxpconn  32375  cvxsconn  32376  cvmsss2  32407  cvmliftlem8  32425  cvmlift3lem6  32457  mrsubrn  32646  msubrn  32662  mvtss  32686  mclsssvlem  32695  mclsax  32702  mclsind  32703  neibastop2lem  33594  tailfb  33611  knoppcnlem10  33727  lindsdom  34755  poimirlem2  34763  poimirlem11  34772  poimirlem19  34780  poimirlem27  34788  poimirlem30  34791  mblfinlem2  34799  itg2addnclem2  34813  itg2gt0cn  34816  ftc1anclem3  34838  ftc1anclem6  34841  ftc1anclem7  34842  ftc1anc  34844  cnresima  34912  istotbnd3  34919  sstotbnd2  34922  totbndbnd  34937  prdsbnd  34941  cntotbnd  34944  ismtyima  34951  heibor1lem  34957  heibor  34969  rrnequiv  34983  lsatlss  36001  cdleme50rnlem  37549  cmpfiiin  39161  isnacs3  39174  eldioph2lem2  39225  fnwe2lem2  39518  lmhmfgima  39551  gneispacern  40355  imo72b2lem0  40383  imo72b2lem2  40385  imo72b2lem1  40389  imo72b2  40393  refsumcn  41154  cncmpmax  41156  elpmrn  41352  climinf  41754  climinf2lem  41854  limsupvaluz2  41886  supcnvlimsup  41888  limsupgtlem  41925  icccncfext  42037  dvsinax  42064  itgsubsticclem  42127  fourierdlem70  42329  fourierdlem82  42341  fge0npnf  42517  sge0resrnlem  42553  sge0isum  42577  sge0seq  42596  meadjiunlem  42615  omeiunle  42667  hoicvr  42698  vonvolmbllem  42810  preimaioomnf  42865  smfco  42945  mgmhmima  43903  aacllem  44736
  Copyright terms: Public domain W3C validator