Theorem frn 5434

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

Syntax hints:   → wi 4   ⊆ wss 3166  ran crn 4676   Fn wfn 5266  ⟶wf 5267

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 5275

This theorem is referenced by:  frnd  5435  fco2  5442  fssxp  5443  fimacnvdisj  5460  f00  5467  f0rn0  5470  f1rn  5482  f1ff1  5489  fimacnv  5709  ffvelcdm  5713  f1ompt  5731  fnfvrnss  5740  rnmptss  5741  fliftrel  5861  fo1stresm  6247  fo2ndresm  6248  1stcof  6249  2ndcof  6250  fo2ndf  6313  tposf2  6354  iunon  6370  smores2  6380  map0b  6774  mapsn  6777  f1imaen2g  6885  phplem4dom  6959  isinfinf  6994  updjudhcoinlf  7182  updjudhcoinrg  7183  casef  7190  unirnioo  10095  frecuzrdgdomlem  10562  frecuzrdgfunlem  10564  frecuzrdgtclt  10566  ennnfonelemrn  12790  ctinf  12801  txuni2  14728  blin2  14904  tgqioo  15027  reeff1o  15245