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

Theorem dffn2 6085
 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 3658 . . 3 ran 𝐹 ⊆ V
21biantru 525 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 5930 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 267 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383  Vcvv 3231   ⊆ wss 3607  ran crn 5144   Fn wfn 5921  ⟶wf 5922 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-in 3614  df-ss 3621  df-f 5930 This theorem is referenced by:  f1cnvcnv  6147  fcoconst  6441  fnressn  6465  fndifnfp  6483  1stcof  7240  2ndcof  7241  fnmpt2  7283  tposfn  7426  tz7.48lem  7581  seqomlem2  7591  mptelixpg  7987  r111  8676  smobeth  9446  inar1  9635  imasvscafn  16244  fucidcl  16672  fucsect  16679  curfcl  16919  curf2ndf  16934  dsmmbas2  20129  frlmsslsp  20183  frlmup1  20185  prdstopn  21479  prdstps  21480  ist0-4  21580  ptuncnv  21658  xpstopnlem2  21662  prdstgpd  21975  prdsxmslem2  22381  curry2ima  29614  fnchoice  39502  fsneqrn  39717  stoweidlem35  40570
 Copyright terms: Public domain W3C validator