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

Theorem dffn3 6207
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 3757 . . 3 ran 𝐹 ⊆ ran 𝐹
21biantru 527 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3 df-f 6045 . 2 (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
42, 3bitr4i 267 1 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wss 3707  ran crn 5259   Fn wfn 6036  wf 6037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-in 3714  df-ss 3721  df-f 6045
This theorem is referenced by:  ffrn  6208  fsn2  6558  fo2ndf  7444  fndmfisuppfi  8444  fndmfifsupp  8445  fin23lem17  9344  fin23lem32  9350  fnct  9543  yoniso  17118  1stckgen  21551  ovolicc2  23482  itg1val2  23642  i1fadd  23653  i1fmul  23654  itg1addlem4  23657  i1fmulc  23661  clwlkclwwlklem2  27115  foresf1o  29642  fcoinver  29717  ofpreima2  29767  locfinreflem  30208  pl1cn  30302  poimirlem29  33743  poimirlem30  33744  itg2addnclem2  33767  mapdcl  37436  wessf1ornlem  39862  unirnmap  39891  fsneqrn  39894  icccncfext  40595  stoweidlem29  40741  stoweidlem31  40743  stoweidlem59  40771  subsaliuncllem  41070  meadjiunlem  41177
  Copyright terms: Public domain W3C validator