Theorem frn 5522

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

Syntax hints:   → wi 4   ⊆ wss 3214  ran crn 4755   Fn wfn 5352  ⟶wf 5353

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 5361

This theorem is referenced by:  frnd  5523  fimass  5530  fco2  5534  fssxp  5535  fimacnvdisj  5556  f00  5564  f0rn0  5567  f1rn  5579  f1ff1  5586  fimacnv  5811  ffvelcdm  5815  f1ompt  5833  fnfvrnss  5842  rnmptss  5843  fliftrel  5971  fo1stresm  6368  fo2ndresm  6369  1stcof  6370  2ndcof  6371  fo2ndf  6436  tposf2  6512  iunon  6528  smores2  6538  map0b  6934  mapsnd  6936  mapsn  6938  f1imaen2g  7046  phplem4dom  7129  isinfinf  7167  updjudhcoinlf  7384  updjudhcoinrg  7385  casef  7392  unirnioo  10328  frecuzrdgdomlem  10806  frecuzrdgfunlem  10808  frecuzrdgtclt  10810  ballotfilemsima  13207  ennnfonelemrn  13258  ctinf  13269  txuni2  15251  blin2  15427  tgqioo  15550  reeff1o  15768  usgredgssen  16287