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

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
StepHypRef Expression
1 ssid 3880 . . 3 ran 𝐹 ⊆ ran 𝐹
21biantru 522 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3 df-f 6192 . 2 (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
42, 3bitr4i 270 1 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator