Theorem dffn3 6092

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 3657	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 525	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 5930	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 267	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 196   ∧ wa 383   ⊆ wss 3607  ran crn 5144   Fn wfn 5921  ⟶wf 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930

This theorem is referenced by:  ffrn  6093  fsn2  6443  fo2ndf  7329  fndmfisuppfi  8328  fndmfifsupp  8329  fin23lem17  9198  fin23lem32  9204  fnct  9397  yoniso  16972  1stckgen  21405  ovolicc2  23336  itg1val2  23496  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  i1fmulc  23515  clwlkclwwlklem2  26966  foresf1o  29469  fcoinver  29544  ofpreima2  29594  locfinreflem  30035  pl1cn  30129  poimirlem29  33568  poimirlem30  33569  itg2addnclem2  33592  mapdcl  37259  wessf1ornlem  39685  unirnmap  39714  fsneqrn  39717  icccncfext  40418  stoweidlem29  40564  stoweidlem31  40566  stoweidlem59  40594  subsaliuncllem  40893  meadjiunlem  41000