Definition df-fun 4790

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5120, dffun3 5121, dffun4 5122, dffun5 5123, dffun6 5125, dffun7 5134, dffun8 5135, and dffun9 5136. (Contributed by SF, 5-Jan-2015.) (Revised by Scott Fenton, 14-Apr-2021.)

Assertion

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

Detailed syntax breakdown of Definition df-fun

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wfun 4776	. 2 wff Fun A
3	1	ccnv 4772	. . . 4 class ◡A
4	1, 3	ccom 4722	. . 3 class (A ∘ ◡A)
5		cid 4764	. . 3 class I
6	4, 5	wss 3258	. 2 wff (A ∘ ◡A) ⊆ I
7	2, 6	wb 176	1 wff (Fun A ↔ (A ∘ ◡A) ⊆ I )

This definition is referenced by:  dffun2  5120  funss  5127  nffun  5131  funi  5138  fun0  5155  f1ococnv2  5310