Theorem frn 5376

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

Syntax hints:   → wi 4   ⊆ wss 3131  ran crn 4629   Fn wfn 5213  ⟶wf 5214

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 5222

This theorem is referenced by:  frnd  5377  fco2  5384  fssxp  5385  fimacnvdisj  5402  f00  5409  f0rn0  5412  f1rn  5424  f1ff1  5431  fimacnv  5648  ffvelcdm  5652  f1ompt  5670  fnfvrnss  5679  rnmptss  5680  fliftrel  5796  fo1stresm  6165  fo2ndresm  6166  1stcof  6167  2ndcof  6168  fo2ndf  6231  tposf2  6272  iunon  6288  smores2  6298  map0b  6690  mapsn  6693  f1imaen2g  6796  phplem4dom  6865  isinfinf  6900  updjudhcoinlf  7082  updjudhcoinrg  7083  casef  7090  unirnioo  9976  frecuzrdgdomlem  10420  frecuzrdgfunlem  10422  frecuzrdgtclt  10424  ennnfonelemrn  12423  ctinf  12434  txuni2  13917  blin2  14093  tgqioo  14208  reeff1o  14355