Theorem dffn2 5737

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

Step	Hyp	Ref	Expression
1		ssv 3523	. . 3
2	1	biantru 505	. 2
3		df-f 5597	. 2
4	2, 3	bitr4i 252	1

Syntax hints:  <->wb 184  /\wa 369  cvv 3109  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589

This theorem is referenced by:  f1cnvcnv  5794  fcoconst  6068  fnressn  6083  fndifnfp  6100  1stcof  6828  2ndcof  6829  fnmpt2  6868  tposfn  7003  tz7.48lem  7125  seqomlem2  7135  mptelixpg  7526  r111  8214  smobeth  8982  inar1  9174  imasvscafn  14934  fucidcl  15334  fucsect  15341  curfcl  15501  curf2ndf  15516  dsmmbas2  18768  frlmsslsp  18829  frlmsslspOLD  18830  frlmup1  18832  prdstopn  20129  prdstps  20130  ist0-4  20230  ptuncnv  20308  xpstopnlem2  20312  prdstgpd  20623  prdsxmslem2  21032  curry2ima  27526  fnchoice  31404  stoweidlem35  31817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-f 5597