Theorem dffn2 6720

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

Syntax hints:   ↔ wb 205   ∧ wa 397  Vcvv 3475   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548

This theorem is referenced by:  f1cnvcnv  6798  fcoconst  7132  fnressn  7156  fndifnfp  7174  1stcof  8005  2ndcof  8006  fnmpo  8055  tposfn  8240  tz7.48lem  8441  seqomlem2  8451  mptelixpg  8929  r111  9770  smobeth  10581  inar1  10770  imasvscafn  17483  fucidcl  17918  fucsect  17925  dfinito3  17955  dftermo3  17956  curfcl  18185  curf2ndf  18200  dsmmbas2  21292  frlmsslsp  21351  frlmup1  21353  prdstopn  23132  prdstps  23133  ist0-4  23233  ptuncnv  23311  xpstopnlem2  23315  prdstgpd  23629  prdsxmslem2  24038  curry2ima  31930  fnchoice  43713  fsneqrn  43910  stoweidlem35  44751