HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-fun 4022
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 4451, dffun3 4452, dffun4 4453, dffun5 4454, dffun6 4456, dffun7 4466, dffun8 4467, and dffun9 4468.
Assertion
Ref Expression
df-fun |- (Fun A <-> (Rel A /\ (A o. `'A) C_ _I ))

Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3 class A
21wfun 4006 . 2 wff Fun A
31wrel 4005 . . 3 wff Rel A
41ccnv 3999 . . . . 5 class `'A
51, 4ccom 4004 . . . 4 class (A o. `'A)
6 cid 3623 . . . 4 class _I
75, 6wss 2662 . . 3 wff (A o. `'A) C_ _I
83, 7wa 382 . 2 wff (Rel A /\ (A o. `'A) C_ _I )
92, 8wb 189 1 wff (Fun A <-> (Rel A /\ (A o. `'A) C_ _I ))
Colors of variables: wff set class
This definition is referenced by:  dffun2 4451  funrel 4458  funss 4459  hbfun 4463  funi 4470  f1ococnv2 4656  dffv2 4733  flimfnei2 15543  cnvcan 16484
Copyright terms: Public domain