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

Theorem dffn3 6735
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 3999 . . 3 ran 𝐹 ⊆ ran 𝐹
21biantru 528 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3 df-f 6553 . 2 (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
42, 3bitr4i 277 1 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wss 3944  ran crn 5679   Fn wfn 6544  wf 6545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789
This theorem depends on definitions:  df-bi 206  df-an 395  df-ss 3961  df-f 6553
This theorem is referenced by:  ffrn  6736  ffrnb  6737  fsn2  7145  coof  7708  offsplitfpar  8124  fo2ndf  8126  suppcoss  8213  fndmfisuppfi  9402  fndmfifsupp  9403  fin23lem17  10363  fin23lem32  10369  fnct  10562  yoniso  18280  psdmplcl  22109  1stckgen  23502  ovolicc2  25495  i1fadd  25668  i1fmul  25669  itg1addlem4  25672  itg1addlem4OLD  25673  i1fmulc  25677  clwlkclwwlklem2  29882  foresf1o  32378  fcoinver  32473  ofpreima2  32533  suppssnn0  32657  locfinreflem  33572  pl1cn  33687  fvineqsneu  37021  poimirlem29  37253  poimirlem30  37254  itg2addnclem2  37276  mapdcl  41256  aks6d1c6isolem2  41778  tfsconcatrev  42919  wessf1ornlem  44697  unirnmap  44720  fsneqrn  44723  icccncfext  45413  stoweidlem29  45555  stoweidlem31  45557  stoweidlem59  45585  subsaliuncllem  45883  meadjiunlem  45991  uniimaprimaeqfv  46859  uniimaelsetpreimafv  46873
  Copyright terms: Public domain W3C validator