Theorem frn 5537

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

Syntax hints:   → wi 4   ⊆ wss 3220  ran crn 4770   Fn wfn 5367  ⟶wf 5368

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 5376

This theorem is referenced by:  frnd  5538  fimass  5545  fco2  5549  fssxp  5550  fimacnvdisj  5571  f00  5579  f0rn0  5582  f1rn  5594  f1ff1  5601  fimacnv  5828  ffvelcdm  5832  f1ompt  5850  fnfvrnss  5859  rnmptss  5860  fliftrel  5988  fo1stresm  6385  fo2ndresm  6386  1stcof  6387  2ndcof  6388  fo2ndf  6453  tposf2  6529  iunon  6545  smores2  6555  map0b  6958  mapsnd  6960  mapsn  6962  f1imaen2g  7070  phplem4dom  7153  isinfinf  7191  updjudhcoinlf  7410  updjudhcoinrg  7411  casef  7418  unirnioo  10354  frecuzrdgdomlem  10832  frecuzrdgfunlem  10834  frecuzrdgtclt  10836  ballotfilemsima  13237  ennnfonelemrn  13288  ctinf  13299  txuni2  15280  blin2  15456  tgqioo  15579  reeff1o  15797  usgredgssen  16317