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

Theorem dffn2 6493
 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 3942 . . 3 ran 𝐹 ⊆ V
21biantru 533 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 6332 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 281 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  Vcvv 3444   ⊆ wss 3884  ran crn 5524   Fn wfn 6323  ⟶wf 6324 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-f 6332 This theorem is referenced by:  f1cnvcnv  6563  fcoconst  6877  fnressn  6901  fndifnfp  6919  1stcof  7705  2ndcof  7706  fnmpo  7753  tposfn  7908  tz7.48lem  8064  seqomlem2  8074  mptelixpg  8486  r111  9192  smobeth  10001  inar1  10190  imasvscafn  16805  fucidcl  17230  fucsect  17237  curfcl  17477  curf2ndf  17492  dsmmbas2  20429  frlmsslsp  20488  frlmup1  20490  prdstopn  22236  prdstps  22237  ist0-4  22337  ptuncnv  22415  xpstopnlem2  22419  prdstgpd  22733  prdsxmslem2  23139  curry2ima  30471  fnchoice  41645  fsneqrn  41827  stoweidlem35  42664
 Copyright terms: Public domain W3C validator