wfn - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer	< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > wfn		Structured version GIF version

Syntax Definition wfn 4820

Description: Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B.)

**Hypotheses**
Ref	Expression
cA	class A
cB	class B

**Assertion**
Ref	Expression
wfn	wff A Fn B

See definition df-fn 4828 for more information.

Colors of variables: wff set class