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

Theorem dffn2 6738
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 4008 . . 3 ran 𝐹 ⊆ V
21biantru 529 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 6565 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 278 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  Vcvv 3480  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  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-f 6565
This theorem is referenced by:  f1cnvcnv  6813  fcoconst  7154  fnressn  7178  fndifnfp  7196  1stcof  8044  2ndcof  8045  fnmpo  8094  tposfn  8280  tz7.48lem  8481  seqomlem2  8491  mptelixpg  8975  r111  9815  smobeth  10626  inar1  10815  imasvscafn  17582  fucidcl  18013  fucsect  18020  dfinito3  18050  dftermo3  18051  curfcl  18277  curf2ndf  18292  dsmmbas2  21757  frlmsslsp  21816  frlmup1  21818  prdstopn  23636  prdstps  23637  ist0-4  23737  ptuncnv  23815  xpstopnlem2  23819  prdstgpd  24133  prdsxmslem2  24542  curry2ima  32718  fnchoice  45034  fsneqrn  45216  stoweidlem35  46050  fucorid2  49058  precofval2  49064
  Copyright terms: Public domain W3C validator