Theorem frn 6348

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

Syntax hints:   → wi 4   ⊆ wss 3828  ran crn 5405   Fn wfn 6181  ⟶wf 6182

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 199  df-an 388  df-f 6190

This theorem is referenced by:  frnd  6349  fco2  6360  fssxp  6361  fimass  6382  fimacnvdisj  6384  f00  6388  f0rn0  6391  f1resf1  6410  foconst  6430  ffvelrn  6672  f1ompt  6696  fnfvrnss  6705  rnmptss  6707  isofr2  6918  fo1stres  7524  fo2ndres  7525  1stcof  7528  2ndcof  7529  fnwelem  7627  tposf2  7716  seqomlem2  7887  oacomf1olem  7987  map0b  8242  mapsnd  8244  fipreima  8621  indexfi  8623  dffi3  8686  oismo  8795  djuin  9137  updjudhcoinlf  9151  updjudhcoinrg  9152  acndom  9267  acndom2  9270  dfac12lem2  9360  dfac12lem3  9361  ackbij1  9454  cfflb  9475  fin23lem40  9567  fin23lem41  9568  isf34lem7  9595  fin1a2lem6  9621  fin1a2lem7  9622  hsmexlem4  9645  hsmexlem5  9646  axdc2lem  9664  axdc3lem2  9667  ttukeylem6  9730  unirnfdomd  9783  pwcfsdom  9799  smobeth  9802  pwfseqlem5  9879  tskurn  10005  wfgru  10032  rpnnen1lem4  12191  rpnnen1lem5  12192  unirnioo  12650  fseqsupcl  13157  fseqsupubi  13158  limsupcl  14685  limsuple  14690  limsupval2  14692  prmreclem6  16107  0ram2  16207  0ramcl  16209  imasdsval2  16639  mrcssv  16737  isacs1i  16780  acsmapd  17640  acsmap2d  17641  gsumval1  17739  dfod2  18446  odcl2  18447  sylow1lem2  18479  efgsfo  18618  gexex  18723  iscyggen2  18750  iscyg3  18755  gsumval3lem1  18773  gsumval3  18775  dprdf1  18899  subgdmdprd  18900  subgdprd  18901  lindfmm  20667  m2cpmmhm  21051  leordtval2  21518  lecldbas  21525  discmp  21704  cmpsub  21706  tgcmp  21707  hauscmplem  21712  2ndcctbss  21761  2ndcsep  21765  comppfsc  21838  kgentop  21848  1stckgen  21860  kgencn2  21863  txuni2  21871  xkoopn  21895  xkouni  21905  xkoccn  21925  ptcnplem  21927  txkgen  21958  xkoco1cn  21963  xkoco2cn  21964  xkococnlem  21965  xkococn  21966  xkoinjcn  21993  hmphdis  22102  zfbas  22202  uzrest  22203  elfm  22253  alexsubALT  22357  symgtgp  22407  submtmd  22410  tsmsxplem1  22458  blin2  22736  imasf1oxms  22796  tgqioo  23105  xrtgioo  23111  metdscn2  23162  iimulcn  23239  icchmeo  23242  xrhmeo  23247  cnheiborlem  23255  tcphex  23517  tchnmfval  23528  fmcfil  23572  causs  23598  ovolficcss  23767  elovolm  23773  ovoliunlem2  23801  volsup  23854  uniioovol  23877  dyadmbllem  23897  dyadmbl  23898  opnmbllem  23899  opnmblALT  23901  volsup2  23903  mbfconstlem  23925  i1fd  23979  i1f1  23988  itg11  23989  itg1addlem4  23997  itg1climres  24012  itg2gt0  24058  limciun  24189  c1liplem1  24290  dvne0f1  24306  dvcnvrelem2  24312  dvcnvre  24313  mdeglt  24356  mdegxrcl  24358  mdegcl  24360  ig1peu  24462  ulmss  24682  reeff1o  24732  efifo  24826  dvlog  24929  efopn  24936  lgamcvg2  25328  dchrisum0fno1  25783  usgredgss  26641  hhssims  28825  shsss  28865  pjrni  29254  imaelshi  29610  foresf1o  30038  fnpreimac  30172  dimkerim  30643  smatrcl  30694  locfinreflem  30739  esumcvg  30980  omssubadd  31194  sitgclbn  31237  eulerpartgbij  31266  eulerpartlemgvv  31270  eulerpartlemgf  31273  ballotlemsima  31410  mrsubf  32254  msubf  32269  mstapst  32284  mclsind  32307  mclsppslem  32320  orderseqlem  32585  norn  32649  icoreunrn  34047  pibt2  34104  ptrecube  34311  poimirlem1  34312  poimirlem3  34314  poimirlem12  34323  poimirlem16  34327  poimirlem32  34343  broucube  34345  heicant  34346  opnmbllem0  34347  mblfinlem1  34348  mblfinlem2  34349  mblfinlem3  34350  mblfinlem4  34351  ismblfin  34352  volsupnfl  34356  ftc1anclem5  34390  ftc1anclem7  34392  ftc1anclem8  34393  ftc1anc  34394  indexdom  34429  sstotbnd  34473  prdsbnd  34491  heibor1lem  34507  heiborlem1  34509  rrnval  34525  reheibor  34537  lsatset  35549  elrfirn  38665  isnacs2  38676  nacsfix  38682  coeq0i  38723  diophrw  38729  dnwech  39022  pwssplit4  39063  hbt  39104  rnmptssf  40926  liminfval2  41459  fourierdlem12  41814  fourierdlem42  41844  fourierdlem54  41855  fourierdlem76  41877  fourierdlem85  41886  fourierdlem88  41889  fourierdlem93  41894  fourierdlem113  41914  hoicvr  42240  vonvolmbl2  42355  vonvol2  42356  fafvelrn  42754  fafv2elrn  42818  mgmplusfreseq  43382  elbigolo1  43959  aacllem  44243