Theorem frn 5289

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

Syntax hints:   → wi 4   ⊆ wss 3076  ran crn 4548   Fn wfn 5126  ⟶wf 5127

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 5135

This theorem is referenced by:  frnd  5290  fco2  5297  fssxp  5298  fimacnvdisj  5315  f00  5322  f0rn0  5325  f1rn  5337  f1ff1  5344  fimacnv  5557  ffvelrn  5561  f1ompt  5579  fnfvrnss  5588  rnmptss  5589  fliftrel  5701  fo1stresm  6067  fo2ndresm  6068  1stcof  6069  2ndcof  6070  fo2ndf  6132  tposf2  6173  iunon  6189  smores2  6199  map0b  6589  mapsn  6592  f1imaen2g  6695  phplem4dom  6764  isinfinf  6799  updjudhcoinlf  6973  updjudhcoinrg  6974  casef  6981  unirnioo  9786  frecuzrdgdomlem  10221  frecuzrdgfunlem  10223  frecuzrdgtclt  10225  ennnfonelemrn  11968  ctinf  11979  txuni2  12464  blin2  12640  tgqioo  12755  reeff1o  12902