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

Theorem dffn2 6675
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 3973 . . 3 ran 𝐹 ⊆ V
21biantru 531 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 6505 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 278 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  Vcvv 3448  wss 3915  ran crn 5639   Fn wfn 6496  wf 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-f 6505
This theorem is referenced by:  f1cnvcnv  6753  fcoconst  7085  fnressn  7109  fndifnfp  7127  1stcof  7956  2ndcof  7957  fnmpo  8006  tposfn  8191  tz7.48lem  8392  seqomlem2  8402  mptelixpg  8880  r111  9718  smobeth  10529  inar1  10718  imasvscafn  17426  fucidcl  17861  fucsect  17868  dfinito3  17898  dftermo3  17899  curfcl  18128  curf2ndf  18143  dsmmbas2  21159  frlmsslsp  21218  frlmup1  21220  prdstopn  22995  prdstps  22996  ist0-4  23096  ptuncnv  23174  xpstopnlem2  23178  prdstgpd  23492  prdsxmslem2  23901  curry2ima  31664  fnchoice  43308  fsneqrn  43506  stoweidlem35  44350
  Copyright terms: Public domain W3C validator