Definition df-fun 3192

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 3526, dffun3 3527, dffun4 3528, dffun5 3529, dffunmo 3531, dffun6 3539, and dffun7 3540.

Assertion

Ref	Expression
df-fun	|- (Fun A <-> (Rel A /\ (A o. `'A) (_ I))

Detailed syntax breakdown of Definition df-fun

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wfun 3176	. 2 wff Fun A
3	1	wrel 3175	. . 3 wff Rel A
4	1	ccnv 3169	. . . . 5 class `'A
5	1, 4	ccom 3174	. . . 4 class (A o. `'A)
6		cid 2831	. . . 4 class I
7	5, 6	wss 2047	. . 3 wff (A o. `'A) (_ I
8	3, 7	wa 223	. 2 wff (Rel A /\ (A o. `'A) (_ I)
9	2, 8	wb 146	1 wff (Fun A <-> (Rel A /\ (A o. `'A) (_ I))

This definition is referenced by:  dffun2 3526  funrel 3533  hbfun 3536  funi 3545  f1ococnv2 3708

Copyright terms: Public domain