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

Theorem frn 6259
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 6102 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 486 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3766  ran crn 5309   Fn wfn 6093  wf 6094
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 198  df-an 385  df-f 6102
This theorem is referenced by:  frnd  6260  fco2  6271  fssxp  6272  fimass  6293  fimacnvdisj  6295  f00  6299  f0rn0  6302  f1resf1  6321  foconst  6339  fimacnv  6566  ffvelrn  6576  f1ompt  6600  fnfvrnss  6609  rnmptss  6611  isofr2  6815  fo1stres  7421  fo2ndres  7422  1stcof  7425  2ndcof  7426  fnwelem  7523  tposf2  7608  seqomlem2  7779  oacomf1olem  7878  map0b  8129  mapsnd  8131  f1imaen2g  8250  domunsncan  8296  fipreima  8508  indexfi  8510  dffi3  8573  oismo  8681  djuin  9024  updjudhcoinlf  9038  updjudhcoinrg  9039  acndom  9154  acndom2  9157  carduniima  9199  dfac12lem2  9248  dfac12lem3  9249  ackbij1  9342  cfflb  9363  fin23lem40  9455  fin23lem41  9456  isf34lem7  9483  fin1a2lem6  9509  fin1a2lem7  9510  hsmexlem4  9533  hsmexlem5  9534  axdc2lem  9552  axdc3lem2  9555  ttukeylem6  9618  unirnfdomd  9671  pwcfsdom  9687  smobeth  9690  pwfseqlem5  9767  tskurn  9893  wfgru  9920  rpnnen1lem4  12032  rpnnen1lem5  12033  unirnioo  12488  fseqsupcl  12996  fseqsupubi  12997  limsupcl  14423  limsuple  14428  limsupval2  14430  prmreclem6  15838  0ram2  15938  0ramcl  15940  imasdsval2  16377  mrcssv  16475  isacs1i  16518  acsmapd  17379  acsmap2d  17380  gsumval1  17478  psgnunilem1  18110  dfod2  18178  odcl2  18179  sylow1lem2  18211  efgsfo  18349  gexex  18453  iscyggen2  18480  iscyg3  18485  gsumval3lem1  18503  gsumval3  18505  dprdf1  18630  subgdmdprd  18631  subgdprd  18632  lindfmm  20372  m2cpmmhm  20759  leordtval2  21226  lecldbas  21233  discmp  21411  cmpsub  21413  tgcmp  21414  hauscmplem  21419  2ndcctbss  21468  2ndcsep  21472  comppfsc  21545  kgentop  21555  1stckgen  21567  kgencn2  21570  txuni2  21578  xkoopn  21602  xkouni  21612  xkoccn  21632  ptcnplem  21634  txkgen  21665  xkoco1cn  21670  xkoco2cn  21671  xkococnlem  21672  xkococn  21673  xkoinjcn  21700  hmphdis  21809  fbasrn  21897  zfbas  21909  uzrest  21910  elfm  21960  imaelfm  21964  alexsubALT  22064  symgtgp  22114  submtmd  22117  tsmsxplem1  22165  blin2  22443  imasf1oxms  22503  tgqioo  22812  xrtgioo  22818  metdscn2  22869  iimulcn  22946  icchmeo  22949  xrhmeo  22954  cnheiborlem  22962  tchex  23224  tchnmfval  23235  fmcfil  23278  causs  23304  ovolficcss  23446  elovolm  23452  ovoliunlem2  23480  volsup  23533  uniioovol  23556  dyadmbllem  23576  dyadmbl  23577  opnmbllem  23578  opnmblALT  23580  volsup2  23582  mbfconstlem  23604  i1fd  23658  i1f1  23667  itg11  23668  itg1addlem4  23676  itg1climres  23691  itg2gt0  23737  limciun  23868  c1liplem1  23969  dvne0f1  23985  dvcnvrelem2  23991  dvcnvre  23992  mdeglt  24035  mdegxrcl  24037  mdegcl  24039  ig1peu  24141  ulmss  24361  reeff1o  24411  efifo  24504  dvlog  24607  efopn  24614  lgamcvg2  24991  dchrisum0fno1  25410  usgredgss  26265  hhssims  28457  shsss  28497  pjrni  28886  imaelshi  29242  foresf1o  29665  fimarab  29769  smatrcl  30184  locfinreflem  30229  esumcvg  30470  omssubadd  30684  sitgclbn  30727  eulerpartgbij  30756  eulerpartlemgvv  30760  eulerpartlemgf  30763  ballotlemsima  30899  mrsubf  31734  msubf  31749  mstapst  31764  mclsind  31787  mclsppslem  31800  orderseqlem  32070  norn  32122  icoreunrn  33520  ptrecube  33719  poimirlem1  33720  poimirlem3  33722  poimirlem12  33731  poimirlem16  33735  poimirlem32  33751  broucube  33753  heicant  33754  opnmbllem0  33755  mblfinlem1  33756  mblfinlem2  33757  mblfinlem3  33758  mblfinlem4  33759  ismblfin  33760  volsupnfl  33764  ftc1anclem5  33798  ftc1anclem7  33800  ftc1anclem8  33801  ftc1anc  33802  indexdom  33838  sstotbnd  33882  prdsbnd  33900  heibor1lem  33916  heiborlem1  33918  rrnval  33934  reheibor  33946  lsatset  34767  elrfirn  37757  isnacs2  37768  nacsfix  37774  coeq0i  37815  diophrw  37821  dnwech  38116  pwssplit4  38157  hbt  38198  rnmptssf  39942  liminfval2  40477  fourierdlem12  40812  fourierdlem42  40842  fourierdlem54  40853  fourierdlem76  40875  fourierdlem85  40884  fourierdlem88  40887  fourierdlem93  40892  fourierdlem113  40912  hoicvr  41241  vonvolmbl2  41356  vonvol2  41357  fafvelrn  41756  fafv2elrn  41820  mgmplusfreseq  42338  elbigolo1  42916  aacllem  43115
  Copyright terms: Public domain W3C validator