Theorem frn 5416

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

Syntax hints:   → wi 4   ⊆ wss 3157  ran crn 4664   Fn wfn 5253  ⟶wf 5254

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 5262

This theorem is referenced by:  frnd  5417  fco2  5424  fssxp  5425  fimacnvdisj  5442  f00  5449  f0rn0  5452  f1rn  5464  f1ff1  5471  fimacnv  5691  ffvelcdm  5695  f1ompt  5713  fnfvrnss  5722  rnmptss  5723  fliftrel  5839  fo1stresm  6219  fo2ndresm  6220  1stcof  6221  2ndcof  6222  fo2ndf  6285  tposf2  6326  iunon  6342  smores2  6352  map0b  6746  mapsn  6749  f1imaen2g  6852  phplem4dom  6923  isinfinf  6958  updjudhcoinlf  7146  updjudhcoinrg  7147  casef  7154  unirnioo  10048  frecuzrdgdomlem  10509  frecuzrdgfunlem  10511  frecuzrdgtclt  10513  ennnfonelemrn  12636  ctinf  12647  txuni2  14492  blin2  14668  tgqioo  14791  reeff1o  15009