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

Theorem frn 6500
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 6338 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 500 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3908  ran crn 5533   Fn wfn 6329  wf 6330
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 210  df-an 400  df-f 6338
This theorem is referenced by:  frnd  6501  fco2  6514  fssxp  6515  fimass  6536  fimacnvdisj  6538  f00  6542  f0rn0  6545  f1resf1  6565  foconst  6585  ffvelrn  6831  f1ompt  6857  fnfvrnss  6866  rnmptss  6868  isofr2  7081  fiun  7630  fo1stres  7701  fo2ndres  7702  1stcof  7705  2ndcof  7706  fnwelem  7812  tposf2  7903  seqomlem2  8074  oacomf1olem  8177  map0b  8434  mapsnd  8437  fipreima  8818  indexfi  8820  dffi3  8883  oismo  8992  djuin  9335  updjudhcoinlf  9349  updjudhcoinrg  9350  acndom  9466  acndom2  9469  dfac12lem2  9559  dfac12lem3  9560  ackbij1  9649  cfflb  9670  fin23lem40  9762  fin23lem41  9763  isf34lem7  9790  fin1a2lem6  9816  fin1a2lem7  9817  hsmexlem4  9840  hsmexlem5  9841  axdc2lem  9859  axdc3lem2  9862  ttukeylem6  9925  unirnfdomd  9978  pwcfsdom  9994  smobeth  9997  pwfseqlem5  10074  tskurn  10200  wfgru  10227  rpnnen1lem4  12367  rpnnen1lem5  12368  unirnioo  12827  fseqsupcl  13340  fseqsupubi  13341  limsupcl  14821  limsuple  14826  limsupval2  14828  prmreclem6  16246  0ram2  16346  0ramcl  16348  imasdsval2  16780  mrcssv  16876  isacs1i  16919  acsmapd  17779  acsmap2d  17780  gsumval1  17884  dfod2  18682  odcl2  18683  sylow1lem2  18715  efgsfo  18856  gexex  18964  iscyggen2  18991  iscyg3  18996  gsumval3lem1  19016  gsumval3  19018  dprdf1  19146  subgdmdprd  19147  subgdprd  19148  lindfmm  20514  m2cpmmhm  21348  leordtval2  21815  lecldbas  21822  discmp  22001  cmpsub  22003  tgcmp  22004  hauscmplem  22009  2ndcctbss  22058  2ndcsep  22062  comppfsc  22135  kgentop  22145  1stckgen  22157  kgencn2  22160  txuni2  22168  xkoopn  22192  xkouni  22202  xkoccn  22222  ptcnplem  22224  txkgen  22255  xkoco1cn  22260  xkoco2cn  22261  xkococnlem  22262  xkococn  22263  xkoinjcn  22290  hmphdis  22399  zfbas  22499  uzrest  22500  elfm  22550  alexsubALT  22654  efmndtmd  22704  submtmd  22707  symgtgp  22709  tsmsxplem1  22756  blin2  23034  imasf1oxms  23094  tgqioo  23403  xrtgioo  23409  metdscn2  23460  iimulcn  23541  icchmeo  23544  xrhmeo  23549  cnheiborlem  23557  tcphex  23819  tchnmfval  23830  fmcfil  23874  causs  23900  ovolficcss  24071  elovolm  24077  ovoliunlem2  24105  volsup  24158  uniioovol  24181  dyadmbllem  24201  dyadmbl  24202  opnmbllem  24203  opnmblALT  24205  volsup2  24207  mbfconstlem  24229  i1fd  24283  i1f1  24292  itg11  24293  itg1addlem4  24301  itg1climres  24316  itg2gt0  24362  limciun  24495  c1liplem1  24597  dvne0f1  24613  dvcnvrelem2  24619  dvcnvre  24620  mdeglt  24664  mdegxrcl  24666  mdegcl  24668  ig1peu  24770  ulmss  24990  reeff1o  25040  efifo  25137  dvlog  25240  efopn  25247  lgamcvg2  25638  dchrisum0fno1  26093  usgredgss  26950  hhssims  29055  shsss  29094  pjrni  29483  imaelshi  29839  foresf1o  30271  fnpreimac  30424  tocyc01  30791  cycpmrn  30816  cycpmconjslem2  30828  cyc3conja  30830  dimkerim  31080  smatrcl  31118  locfinreflem  31162  esumcvg  31419  omssubadd  31632  sitgclbn  31675  eulerpartgbij  31704  eulerpartlemgvv  31708  eulerpartlemgf  31711  ballotlemsima  31847  hashf1dmcdm  32430  lfuhgr  32438  mrsubf  32838  msubf  32853  mstapst  32868  mclsind  32891  mclsppslem  32904  orderseqlem  33168  norn  33232  icoreunrn  34737  pibt2  34795  ptrecube  35015  poimirlem1  35016  poimirlem3  35018  poimirlem12  35027  poimirlem16  35031  poimirlem32  35047  broucube  35049  heicant  35050  opnmbllem0  35051  mblfinlem1  35052  mblfinlem2  35053  mblfinlem3  35054  mblfinlem4  35055  ismblfin  35056  volsupnfl  35060  ftc1anclem5  35092  ftc1anclem7  35094  ftc1anclem8  35095  ftc1anc  35096  indexdom  35130  sstotbnd  35171  prdsbnd  35189  heibor1lem  35205  heiborlem1  35207  rrnval  35223  reheibor  35235  lsatset  36244  elrfirn  39566  isnacs2  39577  nacsfix  39583  coeq0i  39624  diophrw  39630  dnwech  39922  pwssplit4  39963  hbt  40004  rnmptssf  41823  liminfval2  42349  fourierdlem12  42700  fourierdlem42  42730  fourierdlem54  42741  fourierdlem76  42763  fourierdlem85  42772  fourierdlem88  42775  fourierdlem93  42780  fourierdlem113  42800  hoicvr  43126  vonvolmbl2  43241  vonvol2  43242  fafvelrn  43665  fafv2elrn  43729  mgmplusfreseq  44332  elbigolo1  44910  aacllem  45268
  Copyright terms: Public domain W3C validator