Definition df-fun 3199

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 3533, dffun3 3534, dffun4 3535, dffun5 3536, dffunmo 3538, dffun6 3546, and dffun7 3547.

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 3183	. 2 wff Fun A
3	1	wrel 3182	. . 3 wff Rel A
4	1	ccnv 3176	. . . . 5 class `'A
5	1, 4	ccom 3181	. . . 4 class (A o. `'A)
6		cid 2838	. . . 4 class I
7	5, 6	wss 2051	. . 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 3533  funrel 3540  hbfun 3543  funi 3552  f1ococnv2 3715

Copyright terms: Public domain