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

Theorem dffn2 6014
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 3610 . . 3 ran 𝐹 ⊆ V
21biantru 526 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 5861 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 267 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  Vcvv 3190  wss 3560  ran crn 5085   Fn wfn 5852  wf 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3192  df-in 3567  df-ss 3574  df-f 5861
This theorem is referenced by:  f1cnvcnv  6076  fcoconst  6366  fnressn  6390  fndifnfp  6407  1stcof  7156  2ndcof  7157  fnmpt2  7198  tposfn  7341  tz7.48lem  7496  seqomlem2  7506  mptelixpg  7905  r111  8598  smobeth  9368  inar1  9557  imasvscafn  16137  fucidcl  16565  fucsect  16572  curfcl  16812  curf2ndf  16827  dsmmbas2  20021  frlmsslsp  20075  frlmup1  20077  prdstopn  21371  prdstps  21372  ist0-4  21472  ptuncnv  21550  xpstopnlem2  21554  prdstgpd  21868  prdsxmslem2  22274  curry2ima  29370  fnchoice  38710  fsneqrn  38912  stoweidlem35  39589
  Copyright terms: Public domain W3C validator