Theorem frn 2757

Description: The range of a mapping.

Assertion

Ref	Expression
frn	⊢ (F:A–→B → ran F ⊆ B)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 2434	. 2 ⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))
2	1	pm3.27bd 263	1 ⊢ (F:A–→B → ran F ⊆ B)

Syntax hints:   → wi 2   ⊆ wss 1487  ran crn 2411   Fn wfn 2417  –→wf 2418

This theorem is referenced by:  fss 2759  fco 2760  fssxp 2761  f00 2773  f1dmex 2819  ffvrn 2890  fnfvrnss 2893  map0b 3267  mapsn 3269  mapenlem2 3385  inf3lem7 3470  fodomb 3615  carduniima 3695  ruclem17 4901  ruclem33 4917

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-f 2434

metamath.org