Theorem frn 6736

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 6559	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simprbi 503	1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ran crn 5656   Fn wfn 6550  ⟶wf 6551

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 6559

This theorem is used by:  frnd  6737  fimass  6749  fimacnv  6751  fco2  6755  fssxp  6756  fimacnvdisj  6779  f00  6783  f0rn0  6786  f1resf1  6807  foconst  6830  ffvelcdm  7102  f1ompt  7132  fnfvrnss  7142  rnmptss  7144  isofr2  7372  f1we  7383  fiun  7976  fo1stres  8048  fo2ndres  8049  1stcof  8052  2ndcof  8053  fnwelem  8167  orderseqlem  8198  tposf2  8292  seqomlem2  8486  oacomf1olem  8597  naddunif  8728  naddasslem1  8729  naddasslem2  8730  map0b  8936  mapsnd  8939  fipreima  9372  indexfi  9374  dffi3  9447  oismo  9558  djuin  10023  updjudhcoinlf  10037  updjudhcoinrg  10038  acndom  10154  acndom2  10157  dfac12lem2  10247  dfac12lem3  10248  ackbij1  10339  cfflb  10361  fin23lem40  10453  fin23lem41  10454  isf34lem7  10481  fin1a2lem6  10507  fin1a2lem7  10508  hsmexlem4  10531  hsmexlem5  10532  axdc2lem  10550  axdc3lem2  10553  ttukeylem6  10616  unirnfdomd  10676  pwcfsdom  10692  smobeth  10695  pwfseqlem5  10772  tskurn  10898  wfgru  10925  rpnnen1lem4  13132  rpnnen1lem5  13133  unirnioo  13604  fseqsupcl  14144  fseqsupubi  14145  hashf1dmcdm  14613  limsupcl  15666  limsuple  15671  limsupval2  15673  prmreclem6  17125  0ram2  17225  0ramcl  17227  imasdsval2  17714  mrcssv  17814  isacs1i  17857  acsmapd  18754  acsmap2d  18755  gsumval1  18898  dfod2  19805  odcl2  19806  sylow1lem2  19840  efgsfo  19980  gexex  20094  iscyggen2  20122  iscyg3  20127  gsumval3lem1  20146  gsumval3  20148  dprdf1  20276  subgdmdprd  20277  subgdprd  20278  lindfmm  22160  m2cpmmhm  23090  leordtval2  23557  lecldbas  23564  discmp  23743  cmpsub  23745  tgcmp  23746  hauscmplem  23751  2ndcctbss  23801  2ndcsep  23805  comppfsc  23878  kgentop  23888  1stckgen  23900  kgencn2  23903  txuni2  23911  xkoopn  23935  xkouni  23945  xkoccn  23965  ptcnplem  23967  txkgen  23998  xkoco1cn  24003  xkoco2cn  24004  xkococnlem  24005  xkococn  24006  xkoinjcn  24033  hmphdis  24142  zfbas  24242  uzrest  24243  elfm  24293  alexsubALT  24397  efmndtmd  24447  submtmd  24450  symgtgp  24452  tsmsxplem1  24499  blin2  24775  imasf1oxms  24835  tgqioo  25146  xrtgioo  25153  metdscn2  25204  iimulcn  25286  icchmeo  25289  xrhmeo  25294  cnheiborlem  25302  tcphex  25565  tchnmfval  25576  fmcfil  25620  causs  25646  ovolficcss  25817  elovolm  25823  ovoliunlem2  25851  volsup  25904  uniioovol  25927  dyadmbllem  25947  dyadmbl  25948  opnmbllem  25949  opnmblALT  25951  volsup2  25953  mbfconstlem  25975  i1fd  26029  i1f1  26038  itg11  26039  itg1addlem4  26047  itg1climres  26062  itg2gt0  26108  limciun  26241  c1liplem1  26343  dvne0f1  26359  dvcnvrelem2  26365  dvcnvre  26366  mdeglt  26410  mdegxrcl  26412  mdegcl  26414  ig1peu  26520  ulmss  26751  reeff1o  26801  efifo  26902  dvlog  27006  efopn  27013  lgamcvg2  27409  dchrisum0fno1  27865  norn  28035  oldf  28250  lfuhgr  29753  usgredgss  29767  hhssims  31903  shsss  31942  pjrni  32331  imaelshi  32687  foresf1o  33169  fnpreimac  33333  tocyc01  33746  cycpmrn  33771  cycpmconjslem2  33783  cyc3conja  33785  dimkerim  34326  smatrcl  34495  locfinreflem  34539  esumcvg  34785  omssubadd  34999  sitgclbn  35042  eulerpartgbij  35071  eulerpartlemgvv  35075  eulerpartlemgf  35078  ballotlemsima  35215  acwer1prc  35851  jf1o  36010  prconf1acwevd  36047  mrsubf  36448  msubf  36463  mstapst  36478  mclsind  36501  mclsppslem  36514  icoreunrn  38473  ptrecube  38729  poimirlem1  38730  poimirlem3  38732  poimirlem12  38741  poimirlem16  38745  poimirlem32  38761  broucube  38763  heicant  38764  opnmbllem0  38765  mblfinlem1  38766  mblfinlem2  38767  mblfinlem3  38768  mblfinlem4  38769  ismblfin  38770  volsupnfl  38774  ftc1anclem5  38806  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  indexdom  38859  sstotbnd  38900  prdsbnd  38918  heibor1lem  38934  heiborlem1  38936  rrnval  38952  reheibor  38964  lsatset  40238  aks6d1c2  43371  aks6d1c6lem3  43413  aks6d1c6isolem1  43415  aks6d1c7lem1  43421  unitscyglem1  43436  elrfirn  43897  isnacs2  43908  nacsfix  43914  coeq0i  43955  diophrw  43961  pwssplit4  44282  hbt  44322  rnmptssf  46462  rnmptssff  46489  liminfval2  46981  fourierdlem12  47332  fourierdlem42  47362  fourierdlem54  47373  fourierdlem76  47395  fourierdlem85  47404  fourierdlem88  47407  fourierdlem93  47412  hoicvr  47761  vonvolmbl2  47876  vonvol2  47877  fafvelcdm  48443  fafv2elcdm  48507  mgmplusfreseq  49465  elbigolo1  49872  aacllem  51217