# Metamath Proof Explorer

## Definition df-fun

Description: Define predicate that determines if some class A is a function. Definition 10.1 of Quine p. 65. For example, the expression Fun cos is true once we define cosine ( df-cos ). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt with the maps-to notation (see df-mpt and df-mpo ). Contrast this predicate with the predicates to determine if some class is a function with a given domain ( df-fn ), a function with a given domain and codomain ( df-f ), a one-to-one function ( df-f1 ), an onto function ( df-fo ), or a one-to-one onto function ( df-f1o ). For alternate definitions, see dffun2 , dffun3 , dffun4 , dffun5 , dffun6 , dffun7 , dffun8 , and dffun9 . (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion df-fun ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge {A}\circ {{A}}^{-1}\subseteq \mathrm{I}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 wfun ${wff}\mathrm{Fun}{A}$
2 0 wrel ${wff}\mathrm{Rel}{A}$
3 0 ccnv ${class}{{A}}^{-1}$
4 0 3 ccom ${class}\left({A}\circ {{A}}^{-1}\right)$
5 cid ${class}\mathrm{I}$
6 4 5 wss ${wff}{A}\circ {{A}}^{-1}\subseteq \mathrm{I}$
7 2 6 wa ${wff}\left(\mathrm{Rel}{A}\wedge {A}\circ {{A}}^{-1}\subseteq \mathrm{I}\right)$
8 1 7 wb ${wff}\left(\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge {A}\circ {{A}}^{-1}\subseteq \mathrm{I}\right)\right)$