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

Theorem dffn2 5390
 Description: Any function is a mapping into . (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
dffn2

Proof of Theorem dffn2
StepHypRef Expression
1 ssv 3198 . . 3
21biantru 491 . 2
3 df-f 5259 . 2
42, 3bitr4i 243 1
 Colors of variables: wff set class Syntax hints:   wb 176   wa 358  cvv 2788   wss 3152   crn 4690   wfn 5250  wf 5251 This theorem is referenced by:  f1cnvcnv  5445  fcoconst  5695  fnressn  5705  1stcof  6147  2ndcof  6148  fnmpt2  6192  tposfn  6263  tz7.48lem  6453  seqomlem2  6463  mptelixpg  6853  r111  7447  smobeth  8208  inar1  8397  imasvscafn  13439  fucidcl  13839  fucsect  13846  curfcl  14006  curf2ndf  14021  prdstopn  17322  prdstps  17323  ist0-4  17420  ptuncnv  17498  xpstopnlem2  17502  prdstgpd  17807  prdsxmslem2  18075  curry2ima  23247  cbicp  25166  fndifnfp  26756  dsmmbas2  27203  frlmsslsp  27248  frlmup1  27250  fnchoice  27700  stoweidlem35  27784 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790  df-in 3159  df-ss 3166  df-f 5259
 Copyright terms: Public domain W3C validator