Theorem dffn2 6693

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

Step	Hyp	Ref	Expression
1		ssv 3974	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6518	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3450   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-f 6518

This theorem is referenced by:  f1cnvcnv  6768  fcoconst  7109  fnressn  7133  fndifnfp  7153  1stcof  8001  2ndcof  8002  fnmpo  8051  tposfn  8237  tz7.48lem  8412  seqomlem2  8422  mptelixpg  8911  r111  9735  smobeth  10546  inar1  10735  imasvscafn  17507  fucidcl  17937  fucsect  17944  dfinito3  17974  dftermo3  17975  curfcl  18200  curf2ndf  18215  dsmmbas2  21653  frlmsslsp  21712  frlmup1  21714  prdstopn  23522  prdstps  23523  ist0-4  23623  ptuncnv  23701  xpstopnlem2  23705  prdstgpd  24019  prdsxmslem2  24424  curry2ima  32639  onvf1od  35101  fnchoice  45030  fsneqrn  45212  stoweidlem35  46040  ixpv  48882  basresposfo  48970  fucorid2  49356  precofval2  49362