Theorem frn 5498

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

Syntax hints:   → wi 4   ⊆ wss 3201  ran crn 4732   Fn wfn 5328  ⟶wf 5329

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 5337

This theorem is referenced by:  frnd  5499  fimass  5505  fco2  5509  fssxp  5510  fimacnvdisj  5529  f00  5537  f0rn0  5540  f1rn  5552  f1ff1  5559  fimacnv  5784  ffvelcdm  5788  f1ompt  5806  fnfvrnss  5815  rnmptss  5816  fliftrel  5943  fo1stresm  6333  fo2ndresm  6334  1stcof  6335  2ndcof  6336  fo2ndf  6401  tposf2  6477  iunon  6493  smores2  6503  map0b  6899  mapsn  6902  f1imaen2g  7010  phplem4dom  7091  isinfinf  7129  updjudhcoinlf  7339  updjudhcoinrg  7340  casef  7347  unirnioo  10269  frecuzrdgdomlem  10742  frecuzrdgfunlem  10744  frecuzrdgtclt  10746  ennnfonelemrn  13120  ctinf  13131  txuni2  15067  blin2  15243  tgqioo  15366  reeff1o  15584  usgredgssen  16103