Theorem frn 5413

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

Syntax hints:   → wi 4   ⊆ wss 3154  ran crn 4661   Fn wfn 5250  ⟶wf 5251

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 5259

This theorem is referenced by:  frnd  5414  fco2  5421  fssxp  5422  fimacnvdisj  5439  f00  5446  f0rn0  5449  f1rn  5461  f1ff1  5468  fimacnv  5688  ffvelcdm  5692  f1ompt  5710  fnfvrnss  5719  rnmptss  5720  fliftrel  5836  fo1stresm  6216  fo2ndresm  6217  1stcof  6218  2ndcof  6219  fo2ndf  6282  tposf2  6323  iunon  6339  smores2  6349  map0b  6743  mapsn  6746  f1imaen2g  6849  phplem4dom  6920  isinfinf  6955  updjudhcoinlf  7141  updjudhcoinrg  7142  casef  7149  unirnioo  10042  frecuzrdgdomlem  10491  frecuzrdgfunlem  10493  frecuzrdgtclt  10495  ennnfonelemrn  12579  ctinf  12590  txuni2  14435  blin2  14611  tgqioo  14734  reeff1o  14949