Definition df-fun 4789

Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5119, dffun3 5120, dffun4 5121, dffun5 5122, dffun6 5124, dffun7 5133, dffun8 5134, and dffun9 5135. (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 4775	. 2 wff Fun A
3	1	ccnv 4771	. . . 4 class ◡A
4	1, 3	ccom 4721	. . 3 class (A ∘ ◡A)
5		cid 4763	. . 3 class I
6	4, 5	wss 3257	. 2 wff (A ∘ ◡A) ⊆ I
7	2, 6	wb 176	1 wff (Fun A ↔ (A ∘ ◡A) ⊆ I )

This definition is referenced by:  dffun2  5119  funss  5126  nffun  5130  funi  5137  fun0  5154  f1ococnv2  5309