Theorem frn 5491

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

Syntax hints:   → wi 4   ⊆ wss 3200  ran crn 4726   Fn wfn 5321  ⟶wf 5322

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 5330

This theorem is referenced by:  frnd  5492  fimass  5498  fco2  5501  fssxp  5502  fimacnvdisj  5521  f00  5528  f0rn0  5531  f1rn  5543  f1ff1  5550  fimacnv  5776  ffvelcdm  5780  f1ompt  5798  fnfvrnss  5807  rnmptss  5808  fliftrel  5933  fo1stresm  6324  fo2ndresm  6325  1stcof  6326  2ndcof  6327  fo2ndf  6392  tposf2  6434  iunon  6450  smores2  6460  map0b  6856  mapsn  6859  f1imaen2g  6967  phplem4dom  7048  isinfinf  7086  updjudhcoinlf  7279  updjudhcoinrg  7280  casef  7287  unirnioo  10208  frecuzrdgdomlem  10680  frecuzrdgfunlem  10682  frecuzrdgtclt  10684  ennnfonelemrn  13058  ctinf  13069  txuni2  14999  blin2  15175  tgqioo  15298  reeff1o  15516  usgredgssen  16032