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

Theorem frn 6676
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 6501 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 498 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911  ran crn 5635   Fn wfn 6492  wf 6493
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 206  df-an 398  df-f 6501
This theorem is referenced by:  frnd  6677  fimass  6690  fimacnv  6691  fco2  6696  fssxp  6697  fimacnvdisj  6721  f00  6725  f0rn0  6728  f1resf1  6748  foconst  6772  ffvelcdm  7033  f1ompt  7060  fnfvrnss  7069  rnmptss  7071  isofr2  7290  fiun  7876  fo1stres  7948  fo2ndres  7949  1stcof  7952  2ndcof  7953  fnwelem  8064  orderseqlem  8090  tposf2  8182  seqomlem2  8398  oacomf1olem  8512  naddunif  8638  naddasslem1  8639  naddasslem2  8640  map0b  8822  mapsnd  8825  fipreima  9303  indexfi  9305  dffi3  9368  oismo  9477  djuin  9855  updjudhcoinlf  9869  updjudhcoinrg  9870  acndom  9988  acndom2  9991  dfac12lem2  10081  dfac12lem3  10082  ackbij1  10175  cfflb  10196  fin23lem40  10288  fin23lem41  10289  isf34lem7  10316  fin1a2lem6  10342  fin1a2lem7  10343  hsmexlem4  10366  hsmexlem5  10367  axdc2lem  10385  axdc3lem2  10388  ttukeylem6  10451  unirnfdomd  10504  pwcfsdom  10520  smobeth  10523  pwfseqlem5  10600  tskurn  10726  wfgru  10753  rpnnen1lem4  12906  rpnnen1lem5  12907  unirnioo  13367  fseqsupcl  13883  fseqsupubi  13884  limsupcl  15356  limsuple  15361  limsupval2  15363  prmreclem6  16794  0ram2  16894  0ramcl  16896  imasdsval2  17399  mrcssv  17495  isacs1i  17538  acsmapd  18444  acsmap2d  18445  gsumval1  18539  dfod2  19347  odcl2  19348  sylow1lem2  19382  efgsfo  19522  gexex  19632  iscyggen2  19659  iscyg3  19664  gsumval3lem1  19683  gsumval3  19685  dprdf1  19813  subgdmdprd  19814  subgdprd  19815  lindfmm  21236  m2cpmmhm  22097  leordtval2  22566  lecldbas  22573  discmp  22752  cmpsub  22754  tgcmp  22755  hauscmplem  22760  2ndcctbss  22809  2ndcsep  22813  comppfsc  22886  kgentop  22896  1stckgen  22908  kgencn2  22911  txuni2  22919  xkoopn  22943  xkouni  22953  xkoccn  22973  ptcnplem  22975  txkgen  23006  xkoco1cn  23011  xkoco2cn  23012  xkococnlem  23013  xkococn  23014  xkoinjcn  23041  hmphdis  23150  zfbas  23250  uzrest  23251  elfm  23301  alexsubALT  23405  efmndtmd  23455  submtmd  23458  symgtgp  23460  tsmsxplem1  23507  blin2  23785  imasf1oxms  23848  tgqioo  24166  xrtgioo  24172  metdscn2  24223  iimulcn  24304  icchmeo  24307  xrhmeo  24312  cnheiborlem  24320  tcphex  24584  tchnmfval  24595  fmcfil  24639  causs  24665  ovolficcss  24836  elovolm  24842  ovoliunlem2  24870  volsup  24923  uniioovol  24946  dyadmbllem  24966  dyadmbl  24967  opnmbllem  24968  opnmblALT  24970  volsup2  24972  mbfconstlem  24994  i1fd  25048  i1f1  25057  itg11  25058  itg1addlem4  25066  itg1addlem4OLD  25067  itg1climres  25082  itg2gt0  25128  limciun  25261  c1liplem1  25363  dvne0f1  25379  dvcnvrelem2  25385  dvcnvre  25386  mdeglt  25433  mdegxrcl  25435  mdegcl  25437  ig1peu  25539  ulmss  25759  reeff1o  25809  efifo  25906  dvlog  26009  efopn  26016  lgamcvg2  26407  dchrisum0fno1  26862  norn  27002  oldf  27190  usgredgss  28113  hhssims  30219  shsss  30258  pjrni  30647  imaelshi  31003  foresf1o  31434  fnpreimac  31590  tocyc01  31970  cycpmrn  31995  cycpmconjslem2  32007  cyc3conja  32009  dimkerim  32325  smatrcl  32380  locfinreflem  32424  esumcvg  32688  omssubadd  32903  sitgclbn  32946  eulerpartgbij  32975  eulerpartlemgvv  32979  eulerpartlemgf  32982  ballotlemsima  33118  hashf1dmcdm  33711  lfuhgr  33714  mrsubf  34114  msubf  34129  mstapst  34144  mclsind  34167  mclsppslem  34180  icoreunrn  35833  pibt2  35891  ptrecube  36081  poimirlem1  36082  poimirlem3  36084  poimirlem12  36093  poimirlem16  36097  poimirlem32  36113  broucube  36115  heicant  36116  opnmbllem0  36117  mblfinlem1  36118  mblfinlem2  36119  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  volsupnfl  36126  ftc1anclem5  36158  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  indexdom  36196  sstotbnd  36237  prdsbnd  36255  heibor1lem  36271  heiborlem1  36273  rrnval  36289  reheibor  36301  lsatset  37455  elrfirn  41021  isnacs2  41032  nacsfix  41038  coeq0i  41079  diophrw  41085  dnwech  41378  pwssplit4  41419  hbt  41460  rnmptssf  43482  rnmptssff  43510  liminfval2  44016  fourierdlem12  44367  fourierdlem42  44397  fourierdlem54  44408  fourierdlem76  44430  fourierdlem85  44439  fourierdlem88  44442  fourierdlem93  44447  fourierdlem113  44467  hoicvr  44796  vonvolmbl2  44911  vonvol2  44912  fafvelcdm  45409  fafv2elcdm  45473  mgmplusfreseq  46074  elbigolo1  46650  aacllem  47255
  Copyright terms: Public domain W3C validator