Definition df-fun 3273

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 3631, dffun3 3632, dffun4 3633, dffun5 3634, dffun6 3636, dffun7 3644, dffun8 3645, and dffun9 3646.

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 3257	. 2 wff Fun A
3	1	wrel 3256	. . 3 wff Rel A
4	1	ccnv 3250	. . . . 5 class `'A
5	1, 4	ccom 3255	. . . 4 class (A o. `'A)
6		cid 2909	. . . 4 class I
7	5, 6	wss 2099	. . 3 wff (A o. `'A) (_ I
8	3, 7	wa 221	. 2 wff (Rel A /\ (A o. `'A) (_ I)
9	2, 8	wb 144	1 wff (Fun A <-> (Rel A /\ (A o. `'A) (_ I))

This definition is referenced by:  dffun2 3631  funrel 3638  hbfun 3641  funi 3650  f1ococnv2 3819  cnvcan 11814

Copyright terms: Public domain