Theorem frn 5517

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

Syntax hints:   → wi 4   ⊆ wss 3211  ran crn 4750   Fn wfn 5347  ⟶wf 5348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-f 5356

This theorem is referenced by:  frnd  5518  fimass  5525  fco2  5529  fssxp  5530  fimacnvdisj  5551  f00  5559  f0rn0  5562  f1rn  5574  f1ff1  5581  fimacnv  5806  ffvelcdm  5810  f1ompt  5828  fnfvrnss  5837  rnmptss  5838  fliftrel  5965  fo1stresm  6355  fo2ndresm  6356  1stcof  6357  2ndcof  6358  fo2ndf  6423  tposf2  6499  iunon  6515  smores2  6525  map0b  6921  mapsnd  6923  mapsn  6925  f1imaen2g  7033  phplem4dom  7116  isinfinf  7154  updjudhcoinlf  7371  updjudhcoinrg  7372  casef  7379  unirnioo  10306  frecuzrdgdomlem  10779  frecuzrdgfunlem  10781  frecuzrdgtclt  10783  ennnfonelemrn  13170  ctinf  13181  txuni2  15121  blin2  15297  tgqioo  15420  reeff1o  15638  usgredgssen  16157