Theorem dffn3 6355

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 3880	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 522	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6192	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 270	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 198   ∧ wa 387   ⊆ wss 3830  ran crn 5408   Fn wfn 6183  ⟶wf 6184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-in 3837  df-ss 3844  df-f 6192

This theorem is referenced by:  ffrn  6356  fsn2  6721  fo2ndf  7622  fndmfisuppfi  8640  fndmfifsupp  8641  fin23lem17  9558  fin23lem32  9564  fnct  9757  yoniso  17393  1stckgen  21866  ovolicc2  23826  i1fadd  23999  i1fmul  24000  itg1addlem4  24003  i1fmulc  24007  clwlkclwwlklem2  27506  foresf1o  30044  fcoinver  30121  ofpreima2  30173  locfinreflem  30745  pl1cn  30839  fvineqsneu  34130  poimirlem29  34359  poimirlem30  34360  itg2addnclem2  34382  mapdcl  38231  wessf1ornlem  40867  unirnmap  40894  fsneqrn  40897  icccncfext  41598  stoweidlem29  41743  stoweidlem31  41745  stoweidlem59  41773  subsaliuncllem  42069  meadjiunlem  42176