Theorem frn 5371

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

Syntax hints:   → wi 4   ⊆ wss 3129  ran crn 4625   Fn wfn 5208  ⟶wf 5209

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 5217

This theorem is referenced by:  frnd  5372  fco2  5379  fssxp  5380  fimacnvdisj  5397  f00  5404  f0rn0  5407  f1rn  5419  f1ff1  5426  fimacnv  5642  ffvelcdm  5646  f1ompt  5664  fnfvrnss  5673  rnmptss  5674  fliftrel  5788  fo1stresm  6157  fo2ndresm  6158  1stcof  6159  2ndcof  6160  fo2ndf  6223  tposf2  6264  iunon  6280  smores2  6290  map0b  6682  mapsn  6685  f1imaen2g  6788  phplem4dom  6857  isinfinf  6892  updjudhcoinlf  7074  updjudhcoinrg  7075  casef  7082  unirnioo  9967  frecuzrdgdomlem  10410  frecuzrdgfunlem  10412  frecuzrdgtclt  10414  ennnfonelemrn  12410  ctinf  12421  txuni2  13538  blin2  13714  tgqioo  13829  reeff1o  13976