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

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