| Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B.) |
| Ref | Expression |
|---|---|
| cA | class A |
| cB | class B |
| cF | class F |
| Ref | Expression |
|---|---|
| wf | wff F:A–→B |
| Colors of variables: wff set class |