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

Theorem dffn2 6258
Description: Any function is a mapping into V. (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
dffn2 (𝐹 Fn 𝐴𝐹:𝐴⟶V)

Proof of Theorem dffn2
StepHypRef Expression
1 ssv 3822 . . 3 ran 𝐹 ⊆ V
21biantru 521 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 6105 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 269 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  Vcvv 3391  wss 3769  ran crn 5312   Fn wfn 6096  wf 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-v 3393  df-in 3776  df-ss 3783  df-f 6105
This theorem is referenced by:  f1cnvcnv  6325  fcoconst  6624  fnressn  6649  fndifnfp  6667  1stcof  7428  2ndcof  7429  fnmpt2  7471  tposfn  7616  tz7.48lem  7772  seqomlem2  7782  mptelixpg  8182  r111  8885  smobeth  9693  inar1  9882  imasvscafn  16402  fucidcl  16829  fucsect  16836  curfcl  17077  curf2ndf  17092  dsmmbas2  20291  frlmsslsp  20345  frlmup1  20347  prdstopn  21645  prdstps  21646  ist0-4  21746  ptuncnv  21824  xpstopnlem2  21828  prdstgpd  22141  prdsxmslem2  22547  curry2ima  29813  fnchoice  39682  fsneqrn  39890  stoweidlem35  40731
  Copyright terms: Public domain W3C validator