Theorem frn 5204

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

Syntax hints:   → wi 4   ⊆ wss 3013  ran crn 4468   Fn wfn 5044  ⟶wf 5045

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-f 5053

This theorem is referenced by:  frnd  5205  fco2  5212  fssxp  5213  fimacnvdisj  5230  f00  5237  f0rn0  5240  f1rn  5252  f1ff1  5259  fimacnv  5467  ffvelrn  5471  f1ompt  5489  fnfvrnss  5497  rnmptss  5498  fliftrel  5609  fo1stresm  5970  fo2ndresm  5971  1stcof  5972  2ndcof  5973  fo2ndf  6030  tposf2  6071  iunon  6087  smores2  6097  map0b  6484  mapsn  6487  f1imaen2g  6590  phplem4dom  6658  isinfinf  6693  djuin  6836  updjudhcoinlf  6851  updjudhcoinrg  6852  casef  6859  unirnioo  9539  frecuzrdgdomlem  9973  frecuzrdgfunlem  9975  frecuzrdgtclt  9977  blin2  12218  tgqioo  12321