Theorem dffn2 6293

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 3844	. . 3 ⊢ ran 𝐹 ⊆ V
2	1	biantru 525	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
3		df-f 6139	. 2 ⊢ (𝐹:𝐴⟶V ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ V))
4	2, 3	bitr4i 270	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)

Syntax hints:   ↔ wb 198   ∧ wa 386  Vcvv 3398   ⊆ wss 3792  ran crn 5356   Fn wfn 6130  ⟶wf 6131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400  df-in 3799  df-ss 3806  df-f 6139

This theorem is referenced by:  f1cnvcnv  6360  fcoconst  6666  fnressn  6691  fndifnfp  6709  1stcof  7475  2ndcof  7476  fnmpt2  7518  tposfn  7663  tz7.48lem  7819  seqomlem2  7829  mptelixpg  8231  r111  8935  smobeth  9743  inar1  9932  imasvscafn  16583  fucidcl  17010  fucsect  17017  curfcl  17258  curf2ndf  17273  dsmmbas2  20480  frlmsslsp  20539  frlmup1  20541  prdstopn  21840  prdstps  21841  ist0-4  21941  ptuncnv  22019  xpstopnlem2  22023  prdstgpd  22336  prdsxmslem2  22742  curry2ima  30052  fnchoice  40121  fsneqrn  40324  stoweidlem35  41179