HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-fun 3182
Description: Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 3512, dffun3 3513, dffun4 3514, dffun5 3515, dffunmo 3517, dffun6 3525, and dffun7 3526.
Assertion
Ref Expression
df-fun |- (Fun A <-> (Rel A /\ (A o. `'A) (_ I))
Detailed syntax breakdown of Definition df-fun
StepHypRef Expression
1 cA . . 3 class A
21wfun 3166 . 2 wff Fun A
31wrel 3165 . . 3 wff Rel A
41ccnv 3159 . . . . 5 class `'A
51, 4ccom 3164 . . . 4 class (A o. `'A)
6 cid 2820 . . . 4 class I
75, 6wss 2037 . . 3 wff (A o. `'A) (_ I
83, 7wa 223 . 2 wff (Rel A /\ (A o. `'A) (_ I)
92, 8wb 146 1 wff (Fun A <-> (Rel A /\ (A o. `'A) (_ I))
Colors of variables: wff set class
This definition is referenced by:  dffun2 3512  funrel 3519  hbfun 3522  funi 3531  f1ococnv2 3693
Copyright terms: Public domain