Theorem frn 6714

Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
frn	⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 6541	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simprbi 503	1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902  ran crn 5660   Fn wfn 6532  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6541

This theorem is used by:  frnd  6715  fimass  6727  fimacnv  6729  fco2  6733  fssxp  6734  fimacnvdisj  6757  f00  6761  f0rn0  6764  f1resf1  6785  foconst  6808  ffvelcdm  7077  f1ompt  7107  fnfvrnss  7117  rnmptss  7119  isofr2  7348  f1we  7359  fiun  7943  fo1stres  8015  fo2ndres  8016  1stcof  8019  2ndcof  8020  fnwelem  8132  orderseqlem  8158  tposf2  8251  seqomlem2  8443  oacomf1olem  8554  naddunif  8685  naddasslem1  8686  naddasslem2  8687  map0b  8893  mapsnd  8896  fipreima  9328  indexfi  9330  dffi3  9404  oismo  9515  djuin  9926  updjudhcoinlf  9940  updjudhcoinrg  9941  acndom  10057  acndom2  10060  dfac12lem2  10150  dfac12lem3  10151  ackbij1  10242  cfflb  10264  fin23lem40  10356  fin23lem41  10357  isf34lem7  10384  fin1a2lem6  10410  fin1a2lem7  10411  hsmexlem4  10434  hsmexlem5  10435  axdc2lem  10453  axdc3lem2  10456  ttukeylem6  10519  unirnfdomd  10577  pwcfsdom  10593  smobeth  10596  pwfseqlem5  10673  tskurn  10799  wfgru  10826  rpnnen1lem4  13030  rpnnen1lem5  13031  unirnioo  13502  fseqsupcl  14041  fseqsupubi  14042  hashf1dmcdm  14509  limsupcl  15560  limsuple  15565  limsupval2  15567  prmreclem6  17015  0ram2  17115  0ramcl  17117  imasdsval2  17604  mrcssv  17704  isacs1i  17747  acsmapd  18644  acsmap2d  18645  gsumval1  18785  dfod2  19690  odcl2  19691  sylow1lem2  19725  efgsfo  19865  gexex  19979  iscyggen2  20007  iscyg3  20012  gsumval3lem1  20031  gsumval3  20033  dprdf1  20161  subgdmdprd  20162  subgdprd  20163  lindfmm  22039  m2cpmmhm  22969  leordtval2  23436  lecldbas  23443  discmp  23622  cmpsub  23624  tgcmp  23625  hauscmplem  23630  2ndcctbss  23680  2ndcsep  23684  comppfsc  23757  kgentop  23767  1stckgen  23779  kgencn2  23782  txuni2  23790  xkoopn  23814  xkouni  23824  xkoccn  23844  ptcnplem  23846  txkgen  23877  xkoco1cn  23882  xkoco2cn  23883  xkococnlem  23884  xkococn  23885  xkoinjcn  23912  hmphdis  24021  zfbas  24121  uzrest  24122  elfm  24172  alexsubALT  24276  efmndtmd  24326  submtmd  24329  symgtgp  24331  tsmsxplem1  24378  blin2  24654  imasf1oxms  24714  tgqioo  25025  xrtgioo  25032  metdscn2  25083  iimulcn  25165  icchmeo  25168  xrhmeo  25173  cnheiborlem  25181  tcphex  25444  tchnmfval  25455  fmcfil  25499  causs  25525  ovolficcss  25696  elovolm  25702  ovoliunlem2  25730  volsup  25783  uniioovol  25806  dyadmbllem  25826  dyadmbl  25827  opnmbllem  25828  opnmblALT  25830  volsup2  25832  mbfconstlem  25854  i1fd  25908  i1f1  25917  itg11  25918  itg1addlem4  25926  itg1climres  25941  itg2gt0  25987  limciun  26121  c1liplem1  26223  dvne0f1  26239  dvcnvrelem2  26245  dvcnvre  26246  mdeglt  26290  mdegxrcl  26292  mdegcl  26294  ig1peu  26400  ulmss  26628  reeff1o  26678  efifo  26780  dvlog  26884  efopn  26891  lgamcvg2  27287  dchrisum0fno1  27743  norn  27883  oldf  28098  lfuhgr  29589  usgredgss  29603  hhssims  31739  shsss  31778  pjrni  32167  imaelshi  32523  foresf1o  32963  fnpreimac  33128  tocyc01  33543  cycpmrn  33568  cycpmconjslem2  33580  cyc3conja  33582  dimkerim  34122  smatrcl  34291  locfinreflem  34335  esumcvg  34581  omssubadd  34796  sitgclbn  34839  eulerpartgbij  34868  eulerpartlemgvv  34872  eulerpartlemgf  34875  ballotlemsima  35012  mrsubf  36081  msubf  36096  mstapst  36111  mclsind  36134  mclsppslem  36147  icoreunrn  38098  pibt2  38156  ptrecube  38354  poimirlem1  38355  poimirlem3  38357  poimirlem12  38366  poimirlem16  38370  poimirlem32  38386  broucube  38388  heicant  38389  opnmbllem0  38390  mblfinlem1  38391  mblfinlem2  38392  mblfinlem3  38393  mblfinlem4  38394  ismblfin  38395  volsupnfl  38399  ftc1anclem5  38431  ftc1anclem7  38433  ftc1anclem8  38434  ftc1anc  38435  indexdom  38469  sstotbnd  38510  prdsbnd  38528  heibor1lem  38544  heiborlem1  38546  rrnval  38562  reheibor  38574  lsatset  39848  aks6d1c2  42981  aks6d1c6lem3  43023  aks6d1c6isolem1  43025  aks6d1c7lem1  43031  unitscyglem1  43046  elrfirn  43525  isnacs2  43536  nacsfix  43542  coeq0i  43583  diophrw  43589  pwssplit4  43915  hbt  43956  rnmptssf  46061  rnmptssff  46088  liminfval2  46581  fourierdlem12  46932  fourierdlem42  46962  fourierdlem54  46973  fourierdlem76  46995  fourierdlem85  47004  fourierdlem88  47007  fourierdlem93  47012  hoicvr  47361  vonvolmbl2  47476  vonvol2  47477  fafvelcdm  48043  fafv2elcdm  48107  mgmplusfreseq  49065  elbigolo1  49472  aacllem  50754