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

Theorem frn 6091
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frn (𝐹:𝐴𝐵 → ran 𝐹𝐵)

Proof of Theorem frn
StepHypRef Expression
1 df-f 5930 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 479 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607  ran crn 5144   Fn wfn 5921  wf 5922
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 197  df-an 385  df-f 5930
This theorem is referenced by:  fco2  6097  fssxp  6098  fimass  6119  fimacnvdisj  6121  f00  6125  f0rn0  6128  foconst  6164  fimacnv  6387  ffvelrn  6397  f1ompt  6422  fnfvrnss  6430  rnmptss  6432  fliftrel  6598  isofr2  6634  fun11iun  7168  f1dmex  7178  fo1stres  7236  fo2ndres  7237  1stcof  7240  2ndcof  7241  fo2ndf  7329  fnwelem  7337  tposf2  7421  onoviun  7485  onnseq  7486  smores2  7496  seqomlem2  7591  oacomf1olem  7689  map0b  7938  mapsn  7941  f1imaen2g  8058  domdifsn  8084  domunsncan  8101  omxpenlem  8102  fodomr  8152  domss2  8160  f1finf1o  8228  f1fi  8294  unirnffid  8299  fipreima  8313  indexfi  8315  intrnfi  8363  dffi3  8378  ordtypelem8  8471  ordtypelem9  8472  ordtypelem10  8473  oismo  8486  hartogslem1  8488  brwdom2  8519  unxpwdom2  8534  ixpiunwdom  8537  infdifsn  8592  cantnf  8628  ac10ct  8895  numacn  8910  acndom  8912  acndom2  8915  infpwfien  8923  carduniima  8957  dfac12lem2  9004  dfac12lem3  9005  ackbij1  9098  fictb  9105  cfflb  9119  fin23lem40  9211  fin23lem41  9212  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  enfin1ai  9244  fin1a2lem6  9265  fin1a2lem7  9266  hsmexlem4  9289  hsmexlem5  9290  axdc2lem  9308  axdc3lem2  9311  ttukeylem6  9374  unirnfdomd  9427  pwcfsdom  9443  smobeth  9446  canthp1lem2  9513  pwfseqlem5  9523  wuncval2  9607  tskurn  9649  wfgru  9676  peano5nni  11061  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  unirnioo  12311  fseqsupcl  12816  fseqsupubi  12817  hashimarn  13265  hashf1lem1  13277  hashf1lem2  13278  ccatrn  13407  swrdrn  13475  cshwrn  13594  limsupcl  14248  limsupgle  14252  limsuple  14253  limsupval2  14255  limsupgre  14256  isercolllem2  14440  isercoll  14442  isercoll2  14443  climsup  14444  ruclem11  15013  prmreclem6  15672  4sqlem11  15706  vdwapf  15723  vdwlem11  15742  0ram  15771  0ram2  15772  0ramcl  15774  imasdsval2  16223  mrcssv  16321  isacs1i  16365  funcres2b  16604  funcres2c  16608  setcepi  16785  yoniso  16972  isacs4lem  17215  acsmapd  17225  acsmap2d  17226  gsumval1  17324  mhmima  17410  gsumwspan  17430  frmdss2  17447  cycsubgcl  17667  cycsubgss  17668  ghmrn  17720  conjnmz  17741  cntzmhm  17817  f1omvdconj  17912  psgnunilem1  17959  dfod2  18027  odcl2  18028  odf1o2  18034  sylow1lem2  18060  pgpssslw  18075  sylow2blem1  18081  lsmssv  18104  lsmidm  18123  pj1ghm2  18163  efgsp1  18196  efgsfo  18198  efgrelexlemb  18209  cntzcmnf  18294  gexex  18302  iscyggen2  18329  cyggenod  18332  iscyg3  18334  gsumval3eu  18351  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzsubmcl  18364  gsumzaddlem  18367  gsumzadd  18368  gsumzsplit  18373  gsumconst  18380  gsumzoppg  18390  gsumpt  18407  dmdprdd  18444  dprdfcntz  18460  dprdfeq0  18467  dprdlub  18471  dprdres  18473  dprdss  18474  dprdz  18475  dprdf1  18478  subgdmdprd  18479  subgdprd  18480  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  dpjghm2  18509  ablfac1b  18515  lmhmlsp  19097  pj1lmhm2  19149  aspval2  19395  mplcoe5lem  19515  mplbas2  19518  mplind  19550  evlslem1  19563  evlseu  19564  gsumply1subr  19652  pjfo  20107  frlmsplit2  20160  frlmsslsp  20183  frlmlbs  20184  frlmup3  20187  frlmup4  20188  lindff1  20207  lindfrn  20208  f1lindf  20209  lindfmm  20214  indlcim  20227  m2cpmf1  20596  m2cpmghm  20597  m2cpmmhm  20598  iinopn  20755  pptbas  20860  tgrest  21011  resttopon  21013  rest0  21021  restfpw  21031  ordtbaslem  21040  ordtuni  21042  ordtbas2  21043  ordtrest  21054  ordtrest2  21056  leordtval2  21064  lecldbas  21071  cnclsi  21124  cnrest2r  21139  cnprest2  21142  lmss  21150  cncmp  21243  rncmp  21247  discmp  21249  cmpsub  21251  tgcmp  21252  hauscmplem  21257  connima  21276  conncn  21277  2ndcctbss  21306  2ndcdisj  21307  2ndcomap  21309  2ndcsep  21310  dis2ndc  21311  lly1stc  21347  comppfsc  21383  kgentop  21393  kgencmp  21396  1stckgenlem  21404  1stckgen  21405  kgencn2  21408  kgencn3  21409  txuni2  21416  ptbasfi  21432  xkoopn  21440  xkouni  21450  txbasval  21457  xkoccn  21470  ptcnplem  21472  upxp  21474  uptx  21476  txtube  21491  txcmplem1  21492  txcmplem2  21493  tx1stc  21501  txkgen  21503  xkoptsub  21505  xkoco1cn  21508  xkoco2cn  21509  xkococnlem  21510  xkococn  21511  xkoinjcn  21538  hmeores  21622  hmphdis  21647  fbasrn  21735  trfilss  21740  trfg  21742  zfbas  21747  uzrest  21748  elfm  21798  imaelfm  21802  rnelfmlem  21803  fclscmpi  21880  alexsublem  21895  alexsubALT  21902  ptcmplem1  21903  ptcmplem3  21905  cnextcn  21918  tmdgsum2  21947  symgtgp  21952  submtmd  21955  subgtgp  21956  subgntr  21957  opnsubg  21958  clsnsg  21960  tgpconncomp  21963  tsmsfbas  21978  tsmsxplem1  22003  prdsdsf  22219  prdsxmetlem  22220  prdsmet  22222  imasdsf1olem  22225  unirnblps  22271  unirnbl  22272  blin2  22281  imasf1oxms  22341  prdsbl  22343  met1stc  22373  met2ndci  22374  prdsxmslem2  22381  tgqioo  22650  xrtgioo  22656  xrge0gsumle  22683  xrge0tsms  22684  metdcn2  22689  metdsf  22698  metdsge  22699  metdscn2  22707  cnmptre  22773  iimulcn  22784  icchmeo  22787  xrhmeo  22792  cnheiborlem  22800  bndth  22804  evth  22805  evth2  22806  lebnumlem2  22808  lebnumlem3  22809  reparphti  22843  tchex  23062  tchnmfval  23073  fmcfil  23116  causs  23142  bcthlem5  23171  minveclem1  23241  minveclem3b  23245  evthicc2  23275  ovolficcss  23284  elovolm  23289  ovolmge0  23291  ovollb  23293  ovolgelb  23294  ovollb2lem  23302  ovollb2  23303  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovoliun  23319  ovoliun2  23320  ovolscalem1  23327  ovolicc1  23330  ovolicc2lem4  23334  ovolicc2  23336  voliunlem2  23365  voliunlem3  23366  volsup  23370  ioombl1lem2  23373  ioombl1lem4  23375  uniioovol  23393  uniiccvol  23394  uniioombllem1  23395  uniioombllem2  23397  uniioombllem3  23399  uniioombllem6  23402  uniioombl  23403  dyadmbllem  23413  dyadmbl  23414  opnmbllem  23415  opnmblALT  23417  volsup2  23419  vitalilem2  23423  vitalilem4  23425  vitalilem5  23426  mbfconstlem  23441  mbfsup  23476  mbfinf  23477  mbflimsup  23478  i1fima  23490  i1fima2  23491  i1fd  23493  itg1cl  23497  itg1ge0  23498  i1f1  23502  itg11  23503  i1fmullem  23506  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  itg1addlem5  23512  i1fmulc  23515  itg1mulc  23516  i1fres  23517  itg10a  23522  itg1ge0a  23523  itg1climres  23526  mbfi1fseqlem4  23530  itg2seq  23554  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itg2i1fseq2  23568  itg2gt0  23572  itg2cnlem1  23573  itg2cn  23575  limciun  23703  c1liplem1  23804  dvne0  23819  dvne0f1  23820  lhop2  23823  dvcnvrelem2  23826  dvcnvre  23827  mdegleb  23869  mdeglt  23870  mdegldg  23871  mdegxrcl  23872  mdegcl  23874  ig1peu  23976  aalioulem3  24134  ulmss  24196  reeff1o  24246  efifo  24338  dvlog  24442  efopn  24449  logccv  24454  efrlim  24741  lgamcvg2  24826  basellem3  24854  fsumvma  24983  lgseisenlem4  25148  dchrisum0fno1  25245  uhgredgn0  26068  upgredgss  26072  umgredgss  26073  edgupgr  26074  upgredg  26077  usgredgss  26099  usgruspgrb  26121  upgrres1  26250  ubthlem1  27854  minvecolem1  27858  htthlem  27902  hhssims  28260  shsss  28300  pjrni  28689  imaelshi  29045  foresf1o  29469  ofrn  29569  ofrn2  29570  fimarab  29573  xppreima2  29578  fsumiunle  29703  xrge0tsmsd  29913  smatrcl  29990  locfinreflem  30035  cmpcref  30045  ordtrestNEW  30095  ordtrest2NEW  30097  xrge0mulc1cn  30115  rge0scvg  30123  esumcst  30253  esumpfinvallem  30264  esumpcvgval  30268  esumcvg  30276  esumiun  30284  omssubadd  30490  carsggect  30508  sibfinima  30529  sitgclg  30532  sitgclbn  30533  sitgaddlemb  30538  eulerpartgbij  30562  eulerpartlemgvv  30566  eulerpartlemgf  30569  rrvrnss  30637  orvcval4  30650  ballotlemsima  30705  erdsze2lem2  31312  cvxpconn  31350  cvxsconn  31351  cvmsss2  31382  cvmliftlem8  31400  cvmlift3lem6  31432  mrsubrn  31536  mrsubf  31540  msubrn  31552  msubf  31555  mstapst  31570  mvtss  31576  mclsssvlem  31585  mclsax  31592  mclsind  31593  mclsppslem  31606  orderseqlem  31877  norn  31929  neibastop2lem  32480  tailfb  32497  knoppcnlem10  32617  icoreunrn  33337  lindsdom  33533  ptrecube  33539  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem19  33558  poimirlem27  33566  poimirlem30  33569  poimirlem32  33571  broucube  33573  heicant  33574  opnmbllem0  33575  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  volsupnfl  33584  itg2addnclem2  33592  itg2gt0cn  33595  ftc1anclem3  33617  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  indexdom  33659  cnresima  33693  istotbnd3  33700  sstotbnd2  33703  sstotbnd  33704  totbndbnd  33718  prdsbnd  33722  cntotbnd  33725  ismtyima  33732  heibor1lem  33738  heiborlem1  33740  heibor  33750  rrnval  33756  rrnequiv  33764  reheibor  33768  lsatset  34595  lsatlss  34601  cdleme50rnlem  36149  elrfirn  37575  cmpfiiin  37577  isnacs2  37586  isnacs3  37590  nacsfix  37592  coeq0i  37633  diophrw  37639  eldioph2lem2  37641  dnwech  37935  fnwe2lem2  37938  lmhmfgima  37971  pwssplit4  37976  hbt  38017  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  refsumcn  39503  cncmpmax  39505  mapsnd  39702  elpmrn  39728  frnd  39740  rnmptssf  39776  climinf  40156  liminfval2  40318  icccncfext  40418  dvsinax  40445  itgsubsticclem  40509  fourierdlem12  40654  fourierdlem42  40684  fourierdlem54  40695  fourierdlem70  40711  fourierdlem76  40717  fourierdlem82  40723  fourierdlem85  40726  fourierdlem88  40729  fourierdlem93  40734  fourierdlem113  40754  fge0npnf  40902  sge0resrnlem  40938  sge0isum  40962  sge0seq  40981  meadjiunlem  41000  omeiunle  41052  hoicvr  41083  vonvolmbllem  41195  vonvolmbl2  41198  vonvol2  41199  fafvelrn  41571  pfxrn  41718  mgmplusfreseq  42098  mgmhmima  42127  elbigolo1  42676  aacllem  42875
  Copyright terms: Public domain W3C validator