Definition df-f 5259

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 5251	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5250	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4661	. . . 4 class ran 𝐹
7	6, 2	wss 3154	. . 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  5387  feq2  5388  feq3  5389  nff  5401  sbcfg  5403  ffn  5404  dffn2  5406  frn  5413  dffn3  5415  fss  5416  fco  5420  funssxp  5424  fun  5427  fnfco  5429  fssres  5430  fcoi2  5436  fintm  5440  fin  5441  f0  5445  fconst  5450  f1ssr  5467  fof  5477  dff1o2  5506  fun11iun  5522  ffoss  5533  dff2  5703  fmpt  5709  ffnfv  5717  ffvresb  5722  fpr  5741  fprg  5742  idref  5800  dff1o6  5820  fliftf  5843  1stcof  6218  2ndcof  6219  smores  6347  smores2  6349  iordsmo  6352  tfrcllembfn  6412  sbthlemi9  7026  inresflem  7121  frec2uzf1od  10480  frecuzrdgtcl  10486  fclim  11440  ennnfonelemf1  12578  resmhm2b  13064  srgfcl  13472  cnrest2  14415  lmss  14425  psmetxrge0  14511  dvfgg  14867  plyreres  14942  nninfall  15569