Theorem dffn3 6748

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 4006	. . 3 ⊢ ran 𝐹 ⊆ ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3		df-f 6565	. 2 ⊢ (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)

Syntax hints:   ↔ wb 206   ∧ wa 395   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3968  df-f 6565

This theorem is referenced by:  ffrn  6749  ffrnb  6750  fsn2  7156  coof  7721  offsplitfpar  8144  fo2ndf  8146  suppcoss  8232  fndmfisuppfi  9417  fndmfifsupp  9418  fin23lem17  10378  fin23lem32  10384  fnct  10577  yoniso  18330  psdmplcl  22166  1stckgen  23562  ovolicc2  25557  i1fadd  25730  i1fmul  25731  itg1addlem4  25734  i1fmulc  25738  clwlkclwwlklem2  30019  foresf1o  32523  fcoinver  32617  ofpreima2  32676  fmptunsnop  32709  suppssnn0  32809  locfinreflem  33839  pl1cn  33954  fvineqsneu  37412  poimirlem29  37656  poimirlem30  37657  itg2addnclem2  37679  mapdcl  41655  aks6d1c6isolem2  42176  tfsconcatrev  43361  wessf1ornlem  45190  unirnmap  45213  fsneqrn  45216  icccncfext  45902  stoweidlem29  46044  stoweidlem31  46046  stoweidlem59  46074  subsaliuncllem  46372  meadjiunlem  46480  uniimaprimaeqfv  47369  uniimaelsetpreimafv  47383