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

Theorem frnd 6515
Description: Deduction form of frn 6514. 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 6514 . 2 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
31, 2syl 17 1 (𝜑 → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3935  ran crn 5550  wf 6345
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 6353
This theorem is referenced by:  fliftrel  7050  f1iunw  7633  f1iun  7636  f1dmex  7649  fo2ndf  7808  onoviun  7971  onnseq  7972  smores2  7982  domdifsn  8589  omxpenlem  8607  fodomr  8657  domss2  8665  sucdom2  8703  f1finf1o  8734  f1fi  8800  unirnffid  8805  intrnfi  8869  dffi3  8884  ordtypelem8  8978  ordtypelem9  8979  ordtypelem10  8980  hartogslem1  8995  brwdom2  9026  unxpwdom2  9041  ixpiunwdom  9044  infdifsn  9109  cantnf  9145  ac10ct  9449  numacn  9464  infpwfien  9477  fictb  9656  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  enfin1ai  9795  canthp1lem2  10064  gch3  10087  wuncval2  10158  peano5nni  11630  hashimarn  13791  hashf1lem1  13803  hashf1lem2  13804  ccatrn  13933  swrdrn  14004  pfxrn  14037  cshwrn  14154  limsupgle  14824  limsupgre  14828  isercolllem2  15012  isercoll  15014  isercoll2  15015  climsup  15016  ruclem11  15583  4sqlem11  16281  vdwapf  16298  vdwlem11  16317  0ram  16346  funcres2b  17157  funcres2c  17161  setcepi  17338  yoniso  17525  isacs4lem  17768  mhmima  17979  gsumwspan  18001  frmdss2  18018  cycsubm  18285  cycsubgcl  18289  cycsubgss  18290  ghmrn  18311  conjnmz  18332  cntzmhm  18409  f1omvdconj  18505  odf1o2  18629  pgpssslw  18670  sylow2blem1  18676  lsmssv  18699  smndlsmidm  18712  lsmidmOLD  18720  pj1ghm2  18761  efgsp1  18794  efgrelexlemb  18807  cntzcmnf  18896  cyggenod  18934  gsumval3eu  18955  gsumval3lem2  18957  gsumval3  18958  gsumzsubmcl  18969  gsumzaddlem  18972  gsumzadd  18973  gsumzsplit  18978  gsumconst  18985  gsumzoppg  18995  gsumpt  19013  dmdprdd  19052  dprdfcntz  19068  dprdfeq0  19075  dprdlub  19079  dprdres  19081  dprdss  19082  dprdz  19083  subgdprd  19088  dprd2dlem1  19094  dprd2da  19095  dmdprdsplit2lem  19098  dpjghm2  19117  ablfac1b  19123  lmhmlsp  19752  pj1lmhm2  19804  aspval2  20057  mplcoe5lem  20178  mplbas2  20181  mplind  20212  evlslem1  20225  evlseu  20226  gsumply1subr  20332  pjfo  20789  frlmsplit2  20847  frlmsslsp  20870  frlmlbs  20871  frlmup3  20874  frlmup4  20875  lindff1  20894  lindfrn  20895  f1lindf  20896  indlcim  20914  m2cpmf1  21281  m2cpmghm  21282  iinopn  21440  pptbas  21546  tgrest  21697  resttopon  21699  rest0  21707  restfpw  21717  ordtbaslem  21726  ordtuni  21728  ordtbas2  21729  ordtrest  21740  ordtrest2  21742  cnclsi  21810  cnrest2r  21825  cnprest2  21828  lmss  21836  cncmp  21930  rncmp  21934  discmp  21936  connima  21963  conncn  21964  2ndcdisj  21994  2ndcomap  21996  dis2ndc  21998  lly1stc  22034  comppfsc  22070  kgencmp  22083  1stckgenlem  22091  kgencn3  22096  ptbasfi  22119  txbasval  22144  upxp  22161  uptx  22163  txtube  22178  txcmplem1  22179  txcmplem2  22180  tx1stc  22188  xkoptsub  22192  xkoco2cn  22196  xkococnlem  22197  hmeores  22309  fbasrn  22422  trfilss  22427  trfg  22429  uzrest  22435  rnelfmlem  22490  fclscmpi  22567  alexsublem  22582  ptcmplem1  22590  ptcmplem3  22592  cnextcn  22605  tmdgsum2  22634  subgtgp  22643  subgntr  22644  opnsubg  22645  clsnsg  22647  tgpconncomp  22650  tsmsfbas  22665  prdsdsf  22906  prdsxmetlem  22907  prdsmet  22909  imasdsf1olem  22912  unirnblps  22958  unirnbl  22959  prdsbl  23030  met1stc  23060  met2ndci  23061  prdsxmslem2  23068  xrge0gsumle  23370  xrge0tsms  23371  metdcn2  23376  metdsf  23385  metdsge  23386  cnmptre  23460  bndth  23491  evth  23492  evth2  23493  lebnumlem2  23495  lebnumlem3  23496  reparphti  23530  bcthlem5  23860  minveclem1  23956  minveclem3b  23960  evthicc2  23990  ovolmge0  24007  ovollb  24009  ovolgelb  24010  ovollb2lem  24018  ovollb2  24019  ovolunlem1a  24026  ovolunlem1  24027  ovoliunlem1  24032  ovoliun  24035  ovoliun2  24036  ovolscalem1  24043  ovolicc1  24046  ovolicc2lem4  24050  ovolicc2  24052  voliunlem2  24081  voliunlem3  24082  ioombl1lem2  24089  ioombl1lem4  24091  uniioovol  24109  uniiccvol  24110  uniioombllem1  24111  uniioombllem2  24113  uniioombllem3  24115  uniioombllem6  24118  uniioombl  24119  volsup2  24135  vitalilem2  24139  vitalilem4  24141  vitalilem5  24142  mbfsup  24194  mbfinf  24195  mbflimsup  24196  i1fima  24208  i1fima2  24209  itg1cl  24215  itg1ge0  24216  i1fmullem  24224  i1fadd  24225  i1fmul  24226  itg1addlem4  24229  itg1addlem5  24230  i1fmulc  24233  itg1mulc  24234  i1fres  24235  itg10a  24240  itg1ge0a  24241  itg1climres  24244  mbfi1fseqlem4  24248  itg2seq  24272  itg2monolem1  24280  itg2monolem2  24281  itg2monolem3  24282  itg2mono  24283  itg2i1fseq2  24286  itg2gt0  24290  itg2cnlem1  24291  itg2cn  24293  dvne0  24537  lhop2  24541  mdegleb  24587  mdegldg  24589  aalioulem3  24852  logccv  25173  efrlim  25475  basellem3  25588  fsumvma  25717  lgseisenlem4  25882  uhgredgn0  26841  upgredgss  26845  umgredgss  26846  edgupgr  26847  upgredg  26850  usgruspgrb  26894  upgrres1  27023  ubthlem1  28575  minvecolem1  28579  htthlem  28622  ofrn  30315  ofrn2  30316  xppreima2  30324  fsumiunle  30473  xrge0tsmsd  30620  symgcom  30655  cycpmcl  30686  cycpmco2lem1  30696  cycpmco2lem5  30700  cycpmco2  30703  cycpmconjv  30712  cycpmconjslem2  30725  cmpcref  31014  ordtrestNEW  31064  ordtrest2NEW  31066  xrge0mulc1cn  31084  rge0scvg  31092  esumcst  31222  esumpfinvallem  31233  esumpcvgval  31237  esumiun  31253  omssubadd  31458  carsggect  31476  sibfinima  31497  sitgclg  31500  sitgaddlemb  31506  eulerpartgbij  31530  rrvrnss  31605  orvcval4  31618  erdsze2lem2  32349  cvxpconn  32387  cvxsconn  32388  cvmsss2  32419  cvmliftlem8  32437  cvmlift3lem6  32469  mrsubrn  32658  msubrn  32674  mvtss  32698  mclsssvlem  32707  mclsax  32714  mclsind  32715  neibastop2lem  33606  tailfb  33623  knoppcnlem10  33739  lindsdom  34768  poimirlem2  34776  poimirlem11  34785  poimirlem19  34793  poimirlem27  34801  poimirlem30  34804  mblfinlem2  34812  itg2addnclem2  34826  itg2gt0cn  34829  ftc1anclem3  34851  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anc  34857  cnresima  34925  istotbnd3  34932  sstotbnd2  34935  totbndbnd  34950  prdsbnd  34954  cntotbnd  34957  ismtyima  34964  heibor1lem  34970  heibor  34982  rrnequiv  34996  lsatlss  36014  cdleme50rnlem  37562  cmpfiiin  39174  isnacs3  39187  eldioph2lem2  39238  fnwe2lem2  39531  lmhmfgima  39564  gneispacern  40368  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  refsumcn  41167  cncmpmax  41169  elpmrn  41365  climinf  41767  climinf2lem  41867  limsupvaluz2  41899  supcnvlimsup  41901  limsupgtlem  41938  icccncfext  42050  dvsinax  42077  itgsubsticclem  42140  fourierdlem70  42342  fourierdlem82  42354  fge0npnf  42530  sge0resrnlem  42566  sge0isum  42590  sge0seq  42609  meadjiunlem  42628  omeiunle  42680  hoicvr  42711  vonvolmbllem  42823  preimaioomnf  42878  smfco  42958  mgmhmima  43916  aacllem  44800
  Copyright terms: Public domain W3C validator