Definition df-f 2434

Description: Define a function (mapping) with domain and co-domain. Definition 6.15(3) of [TakeutiZaring] p. 27.

Assertion

Ref	Expression
df-f	⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf 2418	. 2 wff F:A–→B
5	3, 1	wfn 2417	. . 3 wff F Fn A
6	3	crn 2411	. . . 4 class ran F
7	6, 2	wss 1487	. . 3 wff ran F ⊆ B
8	5, 7	wa 196	. 2 wff (F Fn A ∧ ran F ⊆ B)
9	4, 8	wb 127	1 wff (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))

This definition is referenced by:  feq1 2748  feq2 2749  feq3 2750  hbf 2751  ffn 2752  fnf 2753  frn 2757  fnfrn 2758  fss 2759  fco 2760  fun 2763  fssres 2764  fint 2769  fin 2770  f0 2772  fconst 2774  fof 2788  f1o2 2804  f1o3 2805  ffoss 2820  fopab2 2891  ffnfv 2892  map0e 3266  sbthlem9 3357  inf3lem6 3469  ac5b 3574  om2uzf1o 4656  ruclem13 4897  infmap2lem2 4952  pjf 5588

metamath.org