Theorem dffn2 6738

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 4008	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6565	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3480   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-f 6565

This theorem is referenced by:  f1cnvcnv  6813  fcoconst  7154  fnressn  7178  fndifnfp  7196  1stcof  8044  2ndcof  8045  fnmpo  8094  tposfn  8280  tz7.48lem  8481  seqomlem2  8491  mptelixpg  8975  r111  9815  smobeth  10626  inar1  10815  imasvscafn  17582  fucidcl  18013  fucsect  18020  dfinito3  18050  dftermo3  18051  curfcl  18277  curf2ndf  18292  dsmmbas2  21757  frlmsslsp  21816  frlmup1  21818  prdstopn  23636  prdstps  23637  ist0-4  23737  ptuncnv  23815  xpstopnlem2  23819  prdstgpd  24133  prdsxmslem2  24542  curry2ima  32718  fnchoice  45034  fsneqrn  45216  stoweidlem35  46050  fucorid2  49058  precofval2  49064