Definition df-fun 2432

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 2674, dffun3 2675, dffun4 2676, dffun5 2677, dffunmo 2679, dffun6 2687, and dffun7 2688.

Assertion

Ref	Expression
df-fun	⊢ (Fun A ↔ (Rel A ∧ (A ∘ ◡A) ⊆ I))

Detailed syntax breakdown of Definition df-fun

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wfun 2416	. 2 wff Fun A
3	1	wrel 2415	. . 3 wff Rel A
4	1	ccnv 2409	. . . . 5 class ◡A
5	1, 4	ccom 2414	. . . 4 class (A ∘ ◡A)
6		cid 2057	. . . 4 class I
7	5, 6	wss 1487	. . 3 wff (A ∘ ◡A) ⊆ I
8	3, 7	wa 196	. 2 wff (Rel A ∧ (A ∘ ◡A) ⊆ I)
9	2, 8	wb 127	1 wff (Fun A ↔ (Rel A ∧ (A ∘ ◡A) ⊆ I))

This definition is referenced by:  dffun2 2674  funrel 2681  hbfun 2684  funi 2692  f1ococnv2 2817

metamath.org