Theorem frn 5281

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

Syntax hints:   → wi 4   ⊆ wss 3071  ran crn 4540   Fn wfn 5118  ⟶wf 5119

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

This theorem depends on definitions:  df-bi 116  df-f 5127

This theorem is referenced by:  frnd  5282  fco2  5289  fssxp  5290  fimacnvdisj  5307  f00  5314  f0rn0  5317  f1rn  5329  f1ff1  5336  fimacnv  5549  ffvelrn  5553  f1ompt  5571  fnfvrnss  5580  rnmptss  5581  fliftrel  5693  fo1stresm  6059  fo2ndresm  6060  1stcof  6061  2ndcof  6062  fo2ndf  6124  tposf2  6165  iunon  6181  smores2  6191  map0b  6581  mapsn  6584  f1imaen2g  6687  phplem4dom  6756  isinfinf  6791  updjudhcoinlf  6965  updjudhcoinrg  6966  casef  6973  unirnioo  9756  frecuzrdgdomlem  10190  frecuzrdgfunlem  10192  frecuzrdgtclt  10194  ennnfonelemrn  11932  ctinf  11943  txuni2  12425  blin2  12601  tgqioo  12716