Definition df-f 5191

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 5183	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5182	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4604	. . . 4 class ran 𝐹
7	6, 2	wss 3115	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 103	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 104	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5319  feq2  5320  feq3  5321  nff  5333  sbcfg  5335  ffn  5336  dffn2  5338  frn  5345  dffn3  5347  fss  5348  fco  5352  funssxp  5356  fun  5359  fnfco  5361  fssres  5362  fcoi2  5368  fintm  5372  fin  5373  f0  5377  fconst  5382  f1ssr  5399  fof  5409  dff1o2  5436  fun11iun  5452  ffoss  5463  dff2  5628  fmpt  5634  ffnfv  5642  ffvresb  5647  fpr  5666  fprg  5667  idref  5724  dff1o6  5743  fliftf  5766  1stcof  6128  2ndcof  6129  smores  6256  smores2  6258  iordsmo  6261  tfrcllembfn  6321  sbthlemi9  6926  inresflem  7021  frec2uzf1od  10337  frecuzrdgtcl  10343  fclim  11231  ennnfonelemf1  12347  cnrest2  12836  lmss  12846  psmetxrge0  12932  dvfgg  13257  nninfall  13849