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

Theorem dffn2 5942
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 3583 . . 3 ran 𝐹 ⊆ V
21biantru 524 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 5790 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 265 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  Vcvv 3168  wss 3535  ran crn 5025   Fn wfn 5781  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-v 3170  df-in 3542  df-ss 3549  df-f 5790
This theorem is referenced by:  f1cnvcnv  6003  fcoconst  6288  fnressn  6304  fndifnfp  6321  1stcof  7060  2ndcof  7061  fnmpt2  7100  tposfn  7241  tz7.48lem  7396  seqomlem2  7406  mptelixpg  7804  r111  8494  smobeth  9260  inar1  9449  imasvscafn  15962  fucidcl  16390  fucsect  16397  curfcl  16637  curf2ndf  16652  dsmmbas2  19838  frlmsslsp  19892  frlmup1  19894  prdstopn  21179  prdstps  21180  ist0-4  21280  ptuncnv  21358  xpstopnlem2  21362  prdstgpd  21676  prdsxmslem2  22081  curry2ima  28671  fnchoice  38010  fsneqrn  38197  stoweidlem35  38728
  Copyright terms: Public domain W3C validator