Theorem frn 5542

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220  ran crn 4775   Fn wfn 5372  ⟶wf 5373

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 5381

This theorem is used by:  frnd  5543  fimass  5550  fco2  5554  fssxp  5555  fimacnvdisj  5576  f00  5584  f0rn0  5587  f1rn  5599  f1ff1  5606  fimacnv  5837  ffvelcdm  5841  f1ompt  5859  fnfvrnss  5868  rnmptss  5869  fliftrel  5998  fo1stresm  6395  fo2ndresm  6396  1stcof  6397  2ndcof  6398  fo2ndf  6463  tposf2  6539  iunon  6555  smores2  6565  map0b  6968  mapsnd  6970  mapsn  6972  f1imaen2g  7080  phplem4dom  7163  isinfinf  7201  updjudhcoinlf  7420  updjudhcoinrg  7421  casef  7428  unirnioo  10375  frecuzrdgdomlem  10854  frecuzrdgfunlem  10856  frecuzrdgtclt  10858  ballotfilemsima  13259  ennnfonelemrn  13310  ctinf  13321  txuni2  15357  blin2  15533  tgqioo  15656  reeff1o  15874  usgredgssen  16403