Theorem frn 5491

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

Syntax hints:   → wi 4   ⊆ wss 3200  ran crn 4726   Fn wfn 5321  ⟶wf 5322

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 5330

This theorem is referenced by:  frnd  5492  fimass  5498  fco2  5501  fssxp  5502  fimacnvdisj  5521  f00  5528  f0rn0  5531  f1rn  5543  f1ff1  5550  fimacnv  5776  ffvelcdm  5780  f1ompt  5798  fnfvrnss  5807  rnmptss  5808  fliftrel  5932  fo1stresm  6323  fo2ndresm  6324  1stcof  6325  2ndcof  6326  fo2ndf  6391  tposf2  6433  iunon  6449  smores2  6459  map0b  6855  mapsn  6858  f1imaen2g  6966  phplem4dom  7047  isinfinf  7085  updjudhcoinlf  7278  updjudhcoinrg  7279  casef  7286  unirnioo  10207  frecuzrdgdomlem  10678  frecuzrdgfunlem  10680  frecuzrdgtclt  10682  ennnfonelemrn  13039  ctinf  13050  txuni2  14979  blin2  15155  tgqioo  15278  reeff1o  15496  usgredgssen  16012