Theorem frn 5454

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

Syntax hints:   → wi 4   ⊆ wss 3174  ran crn 4694   Fn wfn 5285  ⟶wf 5286

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 5294

This theorem is referenced by:  frnd  5455  fco2  5462  fssxp  5463  fimacnvdisj  5482  f00  5489  f0rn0  5492  f1rn  5504  f1ff1  5511  fimacnv  5732  ffvelcdm  5736  f1ompt  5754  fnfvrnss  5763  rnmptss  5764  fliftrel  5884  fo1stresm  6270  fo2ndresm  6271  1stcof  6272  2ndcof  6273  fo2ndf  6336  tposf2  6377  iunon  6393  smores2  6403  map0b  6797  mapsn  6800  f1imaen2g  6908  phplem4dom  6984  isinfinf  7020  updjudhcoinlf  7208  updjudhcoinrg  7209  casef  7216  unirnioo  10130  frecuzrdgdomlem  10599  frecuzrdgfunlem  10601  frecuzrdgtclt  10603  ennnfonelemrn  12905  ctinf  12916  txuni2  14843  blin2  15019  tgqioo  15142  reeff1o  15360