New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-fns		Unicode version

---

Definition df-fns 5762

Description: Define the function with domain relationship. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-fns	Fns

Distinct variable group:   ,

---

Detailed syntax breakdown of Definition df-fns

Step	Hyp	Ref	Expression
1		cfns 5761	. 2 Fns
2		vf	. . . . 5
3	2	cv 1641	. . . 4
4		va	. . . . 5
5	4	cv 1641	. . . 4
6	3, 5	wfn 4776	. . 3
7	6, 2, 4	copab 4622	. 2
8	1, 7	wceq 1642	1 Fns

Colors of variables: wff setvar class

This definition is referenced by:  fnsex  5832  brfns  5833

Copyright terms: Public domain

W3C validator