Definition df-fun 4008

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4431, dffun3 4432, dffun4 4433, dffun5 4434, dffun6 4436, dffun7 4447, dffun8 4448, and dffun9 4450.

Assertion

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

Detailed syntax breakdown of Definition df-fun

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wfun 3992	. 2 wff Fun A
3	1	wrel 3991	. . 3 wff Rel A
4	1	ccnv 3985	. . . . 5 class `'A
5	1, 4	ccom 3990	. . . 4 class (A o. `'A)
6		cid 3582	. . . 4 class _I
7	5, 6	wss 2593	. . 3 wff (A o. `'A) C_ _I
8	3, 7	wa 240	. 2 wff (Rel A /\ (A o. `'A) C_ _I )
9	2, 8	wb 163	1 wff (Fun A <-> (Rel A /\ (A o. `'A) C_ _I ))

This definition is referenced by:  dffun2 4431  funrel 4438  hbfun 4443  funi 4452  f1ococnv2 4662  dffv2 4734  cnvcan 15715

Copyright terms: Public domain