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

Syntax hints:   ↔ wb 205   ∧ wa 394  Vcvv 3463   ⊆ wss 3947  ran crn 5674   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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3465  df-ss 3964  df-f 6548

This theorem is referenced by:  f1cnvcnv  6797  fcoconst  7138  fnressn  7162  fndifnfp  7180  1stcof  8023  2ndcof  8024  fnmpo  8073  tposfn  8260  tz7.48lem  8461  seqomlem2  8471  mptelixpg  8954  r111  9809  smobeth  10618  inar1  10807  imasvscafn  17545  fucidcl  17983  fucsect  17990  dfinito3  18020  dftermo3  18021  curfcl  18250  curf2ndf  18265  dsmmbas2  21729  frlmsslsp  21788  frlmup1  21790  prdstopn  23618  prdstps  23619  ist0-4  23719  ptuncnv  23797  xpstopnlem2  23801  prdstgpd  24115  prdsxmslem2  24524  curry2ima  32618  fnchoice  44663  fsneqrn  44852  stoweidlem35  45690