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  7421  updjudhcoinrg  7422  casef  7429  unirnioo  10386  frecuzrdgdomlem  10869  frecuzrdgfunlem  10871  frecuzrdgtclt  10873  ballotfilemsima  13311  ennnfonelemrn  13362  ctinf  13373  txuni2  15448  blin2  15624  tgqioo  15747  reeff1o  15965  usgredgssen  16569