Definition df-f 5321

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 5313	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5312	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4719	. . . 4 class ran 𝐹
7	6, 2	wss 3197	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 104	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 105	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5455  feq2  5456  feq3  5457  nff  5469  sbcfg  5471  ffn  5472  dffn2  5474  frn  5481  dffn3  5483  fss  5484  fco  5488  funssxp  5492  fun  5496  fnfco  5499  fssres  5500  fcoi2  5506  fintm  5510  fin  5511  f0  5515  fconst  5520  f1ssr  5537  fof  5547  dff1o2  5576  fun11iun  5592  ffoss  5603  dff2  5778  fmpt  5784  ffnfv  5792  ffvresb  5797  fpr  5820  fprg  5821  idref  5879  dff1o6  5899  fliftf  5922  1stcof  6307  2ndcof  6308  smores  6436  smores2  6438  iordsmo  6441  tfrcllembfn  6501  sbthlemi9  7128  inresflem  7223  frec2uzf1od  10623  frecuzrdgtcl  10629  fclim  11800  ennnfonelemf1  12984  resmhm2b  13517  srgfcl  13931  cnrest2  14904  lmss  14914  psmetxrge0  15000  dvfgg  15356  plyreres  15432  ausgrusgrben  15960  ausgrumgrien  15962  nninfall  16334