Theorem dffn2 6672

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

Syntax hints:   ↔ wb 206   ∧ wa 395  Vcvv 3442   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-f 6504

This theorem is referenced by:  f1cnvcnv  6747  fcoconst  7089  fnressn  7113  fndifnfp  7132  1stcof  7973  2ndcof  7974  fnmpo  8023  tposfn  8207  tz7.48lem  8382  seqomlem2  8392  mptelixpg  8885  r111  9699  smobeth  10509  inar1  10698  imasvscafn  17470  fucidcl  17904  fucsect  17911  dfinito3  17941  dftermo3  17942  curfcl  18167  curf2ndf  18182  dsmmbas2  21704  frlmsslsp  21763  frlmup1  21765  prdstopn  23584  prdstps  23585  ist0-4  23685  ptuncnv  23763  xpstopnlem2  23767  prdstgpd  24081  prdsxmslem2  24485  curry2ima  32798  mplvrpmrhm  33723  onvf1od  35320  fnchoice  45383  fsneqrn  45563  stoweidlem35  46387  ixpv  49243  basresposfo  49331  fucorid2  49716  precofval2  49722