Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffn3 Structured version   Visualization version   GIF version

Theorem dffn3 6500
 Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.)
Assertion
Ref Expression
dffn3 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)

Proof of Theorem dffn3
StepHypRef Expression
1 ssid 3937 . . 3 ran 𝐹 ⊆ ran 𝐹
21biantru 533 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3 df-f 6329 . 2 (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
42, 3bitr4i 281 1 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ⊆ wss 3881  ran crn 5521   Fn wfn 6320  ⟶wf 6321 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6329 This theorem is referenced by:  ffrn  6501  fsn2  6876  offsplitfpar  7801  fo2ndf  7803  suppcoss  7857  fndmfisuppfi  8832  fndmfifsupp  8833  fin23lem17  9752  fin23lem32  9758  fnct  9951  yoniso  17530  1stckgen  22169  ovolicc2  24136  i1fadd  24309  i1fmul  24310  itg1addlem4  24313  i1fmulc  24317  clwlkclwwlklem2  27795  foresf1o  30283  fcoinver  30380  ofpreima2  30439  locfinreflem  31208  pl1cn  31323  fvineqsneu  34847  poimirlem29  35105  poimirlem30  35106  itg2addnclem2  35128  mapdcl  38968  wessf1ornlem  41854  unirnmap  41880  fsneqrn  41883  icccncfext  42572  stoweidlem29  42714  stoweidlem31  42716  stoweidlem59  42744  subsaliuncllem  43040  meadjiunlem  43147  uniimaprimaeqfv  43942  uniimaelsetpreimafv  43956
 Copyright terms: Public domain W3C validator