Theorem frn 5346

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

Syntax hints:   → wi 4   ⊆ wss 3116  ran crn 4605   Fn wfn 5183  ⟶wf 5184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-f 5192

This theorem is referenced by:  frnd  5347  fco2  5354  fssxp  5355  fimacnvdisj  5372  f00  5379  f0rn0  5382  f1rn  5394  f1ff1  5401  fimacnv  5614  ffvelrn  5618  f1ompt  5636  fnfvrnss  5645  rnmptss  5646  fliftrel  5760  fo1stresm  6129  fo2ndresm  6130  1stcof  6131  2ndcof  6132  fo2ndf  6195  tposf2  6236  iunon  6252  smores2  6262  map0b  6653  mapsn  6656  f1imaen2g  6759  phplem4dom  6828  isinfinf  6863  updjudhcoinlf  7045  updjudhcoinrg  7046  casef  7053  unirnioo  9909  frecuzrdgdomlem  10352  frecuzrdgfunlem  10354  frecuzrdgtclt  10356  ennnfonelemrn  12352  ctinf  12363  txuni2  12896  blin2  13072  tgqioo  13187  reeff1o  13334