Theorem frn 5545

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220  ran crn 4777   Fn wfn 5375  ⟶wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-f 5384

This theorem is used by:  frnd  5546  fimass  5553  fco2  5557  fssxp  5558  fimacnvdisj  5579  f00  5587  f0rn0  5590  f1rn  5602  f1ff1  5609  fimacnv  5840  ffvelcdm  5844  f1ompt  5862  fnfvrnss  5871  rnmptss  5872  fliftrel  6001  fo1stresm  6399  fo2ndresm  6400  1stcof  6401  2ndcof  6402  fo2ndf  6467  tposf2  6543  iunon  6559  smores2  6569  map0b  6972  mapsnd  6974  mapsn  6976  f1imaen2g  7084  phplem4dom  7167  isinfinf  7205  updjudhcoinlf  7426  updjudhcoinrg  7427  casef  7434  unirnioo  10392  frecuzrdgdomlem  10875  frecuzrdgfunlem  10877  frecuzrdgtclt  10879  ballotfilemsima  13317  ennnfonelemrn  13368  ctinf  13379  txuni2  15482  blin2  15658  tgqioo  15781  reeff1o  15999  usgredgssen  16608