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

Theorem dffn2 6293
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 3844 . . 3 ran 𝐹 ⊆ V
21biantru 525 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3 df-f 6139 . 2 (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
42, 3bitr4i 270 1 (𝐹 Fn 𝐴𝐹:𝐴⟶V)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  Vcvv 3398  wss 3792  ran crn 5356   Fn wfn 6130  wf 6131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400  df-in 3799  df-ss 3806  df-f 6139
This theorem is referenced by:  f1cnvcnv  6360  fcoconst  6666  fnressn  6691  fndifnfp  6709  1stcof  7475  2ndcof  7476  fnmpt2  7518  tposfn  7663  tz7.48lem  7819  seqomlem2  7829  mptelixpg  8231  r111  8935  smobeth  9743  inar1  9932  imasvscafn  16583  fucidcl  17010  fucsect  17017  curfcl  17258  curf2ndf  17273  dsmmbas2  20480  frlmsslsp  20539  frlmup1  20541  prdstopn  21840  prdstps  21841  ist0-4  21941  ptuncnv  22019  xpstopnlem2  22023  prdstgpd  22336  prdsxmslem2  22742  curry2ima  30052  fnchoice  40121  fsneqrn  40324  stoweidlem35  41179
  Copyright terms: Public domain W3C validator