Theorem frn 5356

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

Syntax hints:   → wi 4   ⊆ wss 3121  ran crn 4612   Fn wfn 5193  ⟶wf 5194

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 5202

This theorem is referenced by:  frnd  5357  fco2  5364  fssxp  5365  fimacnvdisj  5382  f00  5389  f0rn0  5392  f1rn  5404  f1ff1  5411  fimacnv  5625  ffvelrn  5629  f1ompt  5647  fnfvrnss  5656  rnmptss  5657  fliftrel  5771  fo1stresm  6140  fo2ndresm  6141  1stcof  6142  2ndcof  6143  fo2ndf  6206  tposf2  6247  iunon  6263  smores2  6273  map0b  6665  mapsn  6668  f1imaen2g  6771  phplem4dom  6840  isinfinf  6875  updjudhcoinlf  7057  updjudhcoinrg  7058  casef  7065  unirnioo  9930  frecuzrdgdomlem  10373  frecuzrdgfunlem  10375  frecuzrdgtclt  10377  ennnfonelemrn  12374  ctinf  12385  txuni2  13050  blin2  13226  tgqioo  13341  reeff1o  13488