Theorem dffn3 4666

Description: A function maps to its range.

Assertion

Ref	Expression
dffn3	|- (F Fn A <-> F:A-->ran F)

Proof of Theorem dffn3

Step	Hyp	Ref	Expression
1		ssid 2863	. . 3 |- ran F C_ ran F
2	1	biantru 953	. 2 |- (F Fn A <-> (F Fn A /\ ran F C_ ran F))
3		df-f 4143	. 2 |- (F:A-->ran F <-> (F Fn A /\ ran F C_ ran F))
4	2, 3	bitr4i 283	1 |- (F Fn A <-> F:A-->ran F)

Syntax hints:   <-> wb 219   /\ wa 337   C_ wss 2827  ran crn 4120   Fn wfn 4126  -->wf 4127

This theorem is referenced by:  fsn2 4903  ac6lem 6324  fodom 6374  cncffvrn 8933  bcthlem33 10175  ghomgrpilem2 14366  domrancur1c 15289  cnresima 16715

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-10 1596  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-in 2834  df-ss 2836  df-f 4143

Copyright terms: Public domain