Theorem frn 6713

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ran crn 5656   Fn wfn 6530  ⟶wf 6531

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 6539

This theorem is used by:  frnd  6714  fimass  6726  fimacnv  6728  fco2  6732  fssxp  6733  fimacnvdisj  6756  f00  6760  f0rn0  6763  f1resf1  6784  foconst  6807  ffvelcdm  7077  f1ompt  7107  fnfvrnss  7117  rnmptss  7119  isofr2  7348  f1we  7359  fiun  7946  fo1stres  8018  fo2ndres  8019  1stcof  8022  2ndcof  8023  fnwelem  8134  orderseqlem  8160  tposf2  8253  seqomlem2  8447  oacomf1olem  8558  naddunif  8689  naddasslem1  8690  naddasslem2  8691  map0b  8897  mapsnd  8900  fipreima  9332  indexfi  9334  dffi3  9408  oismo  9519  djuin  9948  updjudhcoinlf  9962  updjudhcoinrg  9963  acndom  10079  acndom2  10082  dfac12lem2  10172  dfac12lem3  10173  ackbij1  10264  cfflb  10286  fin23lem40  10378  fin23lem41  10379  isf34lem7  10406  fin1a2lem6  10432  fin1a2lem7  10433  hsmexlem4  10456  hsmexlem5  10457  axdc2lem  10475  axdc3lem2  10478  ttukeylem6  10541  unirnfdomd  10601  pwcfsdom  10617  smobeth  10620  pwfseqlem5  10697  tskurn  10823  wfgru  10850  rpnnen1lem4  13055  rpnnen1lem5  13056  unirnioo  13527  fseqsupcl  14066  fseqsupubi  14067  hashf1dmcdm  14534  limsupcl  15585  limsuple  15590  limsupval2  15592  prmreclem6  17038  0ram2  17138  0ramcl  17140  imasdsval2  17627  mrcssv  17727  isacs1i  17770  acsmapd  18667  acsmap2d  18668  gsumval1  18811  dfod2  19717  odcl2  19718  sylow1lem2  19752  efgsfo  19892  gexex  20006  iscyggen2  20034  iscyg3  20039  gsumval3lem1  20058  gsumval3  20060  dprdf1  20188  subgdmdprd  20189  subgdprd  20190  lindfmm  22072  m2cpmmhm  23002  leordtval2  23469  lecldbas  23476  discmp  23655  cmpsub  23657  tgcmp  23658  hauscmplem  23663  2ndcctbss  23713  2ndcsep  23717  comppfsc  23790  kgentop  23800  1stckgen  23812  kgencn2  23815  txuni2  23823  xkoopn  23847  xkouni  23857  xkoccn  23877  ptcnplem  23879  txkgen  23910  xkoco1cn  23915  xkoco2cn  23916  xkococnlem  23917  xkococn  23918  xkoinjcn  23945  hmphdis  24054  zfbas  24154  uzrest  24155  elfm  24205  alexsubALT  24309  efmndtmd  24359  submtmd  24362  symgtgp  24364  tsmsxplem1  24411  blin2  24687  imasf1oxms  24747  tgqioo  25058  xrtgioo  25065  metdscn2  25116  iimulcn  25198  icchmeo  25201  xrhmeo  25206  cnheiborlem  25214  tcphex  25477  tchnmfval  25488  fmcfil  25532  causs  25558  ovolficcss  25729  elovolm  25735  ovoliunlem2  25763  volsup  25816  uniioovol  25839  dyadmbllem  25859  dyadmbl  25860  opnmbllem  25861  opnmblALT  25863  volsup2  25865  mbfconstlem  25887  i1fd  25941  i1f1  25950  itg11  25951  itg1addlem4  25959  itg1climres  25974  itg2gt0  26020  limciun  26153  c1liplem1  26255  dvne0f1  26271  dvcnvrelem2  26277  dvcnvre  26278  mdeglt  26322  mdegxrcl  26324  mdegcl  26326  ig1peu  26432  ulmss  26665  reeff1o  26715  efifo  26816  dvlog  26920  efopn  26927  lgamcvg2  27323  dchrisum0fno1  27779  norn  27919  oldf  28134  lfuhgr  29637  usgredgss  29651  hhssims  31787  shsss  31826  pjrni  32215  imaelshi  32571  foresf1o  33011  fnpreimac  33175  tocyc01  33590  cycpmrn  33615  cycpmconjslem2  33627  cyc3conja  33629  dimkerim  34170  smatrcl  34339  locfinreflem  34383  esumcvg  34629  omssubadd  34844  sitgclbn  34887  eulerpartgbij  34916  eulerpartlemgvv  34920  eulerpartlemgf  34923  ballotlemsima  35060  mrsubf  36179  msubf  36194  mstapst  36209  mclsind  36232  mclsppslem  36245  icoreunrn  38178  pibt2  38236  ptrecube  38434  poimirlem1  38435  poimirlem3  38437  poimirlem12  38446  poimirlem16  38450  poimirlem32  38466  broucube  38468  heicant  38469  opnmbllem0  38470  mblfinlem1  38471  mblfinlem2  38472  mblfinlem3  38473  mblfinlem4  38474  ismblfin  38475  volsupnfl  38479  ftc1anclem5  38511  ftc1anclem7  38513  ftc1anclem8  38514  ftc1anc  38515  indexdom  38549  sstotbnd  38590  prdsbnd  38608  heibor1lem  38624  heiborlem1  38626  rrnval  38642  reheibor  38654  lsatset  39928  aks6d1c2  43061  aks6d1c6lem3  43103  aks6d1c6isolem1  43105  aks6d1c7lem1  43111  unitscyglem1  43126  elrfirn  43605  isnacs2  43616  nacsfix  43622  coeq0i  43663  diophrw  43669  pwssplit4  43995  hbt  44036  rnmptssf  46141  rnmptssff  46168  liminfval2  46661  fourierdlem12  47012  fourierdlem42  47042  fourierdlem54  47053  fourierdlem76  47075  fourierdlem85  47084  fourierdlem88  47087  fourierdlem93  47092  hoicvr  47441  vonvolmbl2  47556  vonvol2  47557  fafvelcdm  48123  fafv2elcdm  48187  mgmplusfreseq  49145  elbigolo1  49552  aacllem  50837