Theorem frn 5522

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

Syntax hints:   → wi 4   ⊆ wss 3214  ran crn 4755   Fn wfn 5352  ⟶wf 5353

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 5361

This theorem is referenced by:  frnd  5523  fimass  5530  fco2  5534  fssxp  5535  fimacnvdisj  5556  f00  5564  f0rn0  5567  f1rn  5579  f1ff1  5586  fimacnv  5811  ffvelcdm  5815  f1ompt  5833  fnfvrnss  5842  rnmptss  5843  fliftrel  5971  fo1stresm  6368  fo2ndresm  6369  1stcof  6370  2ndcof  6371  fo2ndf  6436  tposf2  6512  iunon  6528  smores2  6538  map0b  6934  mapsnd  6936  mapsn  6938  f1imaen2g  7046  phplem4dom  7129  isinfinf  7167  updjudhcoinlf  7384  updjudhcoinrg  7385  casef  7392  unirnioo  10325  frecuzrdgdomlem  10803  frecuzrdgfunlem  10805  frecuzrdgtclt  10807  ballotfilemsima  13203  ennnfonelemrn  13254  ctinf  13265  txuni2  15247  blin2  15423  tgqioo  15546  reeff1o  15764  usgredgssen  16283