Theorem dffn3 6735

Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.)

Assertion

Ref	Expression
dffn3	⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Proof of Theorem dffn3

Step	Hyp	Ref	Expression
1		ssid 3999	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 528	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6553	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 277	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 205   ∧ wa 394   ⊆ wss 3944  ran crn 5679   Fn wfn 6544  ⟶wf 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789

This theorem depends on definitions:  df-bi 206  df-an 395  df-ss 3961  df-f 6553

This theorem is referenced by:  ffrn  6736  ffrnb  6737  fsn2  7145  coof  7708  offsplitfpar  8124  fo2ndf  8126  suppcoss  8213  fndmfisuppfi  9402  fndmfifsupp  9403  fin23lem17  10363  fin23lem32  10369  fnct  10562  yoniso  18280  psdmplcl  22109  1stckgen  23502  ovolicc2  25495  i1fadd  25668  i1fmul  25669  itg1addlem4  25672  itg1addlem4OLD  25673  i1fmulc  25677  clwlkclwwlklem2  29882  foresf1o  32378  fcoinver  32473  ofpreima2  32533  suppssnn0  32657  locfinreflem  33572  pl1cn  33687  fvineqsneu  37021  poimirlem29  37253  poimirlem30  37254  itg2addnclem2  37276  mapdcl  41256  aks6d1c6isolem2  41778  tfsconcatrev  42919  wessf1ornlem  44697  unirnmap  44720  fsneqrn  44723  icccncfext  45413  stoweidlem29  45555  stoweidlem31  45557  stoweidlem59  45585  subsaliuncllem  45883  meadjiunlem  45991  uniimaprimaeqfv  46859  uniimaelsetpreimafv  46873