Theorem frn 5436

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

Syntax hints:   → wi 4   ⊆ wss 3166  ran crn 4677   Fn wfn 5267  ⟶wf 5268

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 5276

This theorem is referenced by:  frnd  5437  fco2  5444  fssxp  5445  fimacnvdisj  5462  f00  5469  f0rn0  5472  f1rn  5484  f1ff1  5491  fimacnv  5711  ffvelcdm  5715  f1ompt  5733  fnfvrnss  5742  rnmptss  5743  fliftrel  5863  fo1stresm  6249  fo2ndresm  6250  1stcof  6251  2ndcof  6252  fo2ndf  6315  tposf2  6356  iunon  6372  smores2  6382  map0b  6776  mapsn  6779  f1imaen2g  6887  phplem4dom  6961  isinfinf  6996  updjudhcoinlf  7184  updjudhcoinrg  7185  casef  7192  unirnioo  10097  frecuzrdgdomlem  10564  frecuzrdgfunlem  10566  frecuzrdgtclt  10568  ennnfonelemrn  12823  ctinf  12834  txuni2  14761  blin2  14937  tgqioo  15060  reeff1o  15278