Definition df-fun 4141

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4535, dffun3 4536, dffun4 4537, dffun5 4538, dffun6 4540, dffun7 4550, dffun8 4551, and dffun9 4552.

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 4125	. 2 wff Fun A
3	1	wrel 4124	. . 3 wff Rel A
4	1	ccnv 4118	. . . . 5 class `'A
5	1, 4	ccom 4123	. . . 4 class (A o. `'A)
6		cid 3743	. . . 4 class _I
7	5, 6	wss 2827	. . 3 wff (A o. `'A) C_ _I
8	3, 7	wa 337	. 2 wff (Rel A /\ (A o. `'A) C_ _I )
9	2, 8	wb 219	1 wff (Fun A <-> (Rel A /\ (A o. `'A) C_ _I ))

This definition is referenced by:  dffun2 4535  funrel 4542  hbfun 4547  funi 4554  f1ococnv2 4745  dffv2 4820  cnvcan 16539

Copyright terms: Public domain