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

Theorem dffn2 6720
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 4004 . . 3 ran 𝐹 ⊆ V
21biantru 528 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 6548 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 277 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  Vcvv 3463  wss 3947  ran crn 5674   Fn wfn 6539  wf 6540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3465  df-ss 3964  df-f 6548
This theorem is referenced by:  f1cnvcnv  6797  fcoconst  7138  fnressn  7162  fndifnfp  7180  1stcof  8023  2ndcof  8024  fnmpo  8073  tposfn  8260  tz7.48lem  8461  seqomlem2  8471  mptelixpg  8954  r111  9809  smobeth  10618  inar1  10807  imasvscafn  17545  fucidcl  17983  fucsect  17990  dfinito3  18020  dftermo3  18021  curfcl  18250  curf2ndf  18265  dsmmbas2  21729  frlmsslsp  21788  frlmup1  21790  prdstopn  23618  prdstps  23619  ist0-4  23719  ptuncnv  23797  xpstopnlem2  23801  prdstgpd  24115  prdsxmslem2  24524  curry2ima  32618  fnchoice  44663  fsneqrn  44852  stoweidlem35  45690
  Copyright terms: Public domain W3C validator