Metamath Proof Explorer

Definition df-funs

Description: Define the class of all functions. See elfuns for membership. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Assertion df-funs 
|- Funs = ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfuns 
 |-  Funs
1 cvv 
 |-  _V
2 1 1 cxp 
 |-  ( _V X. _V )
3 2 cpw 
 |-  ~P ( _V X. _V )
4 cep 
 |-  _E
5 c1st 
 |-  1st
6 cid 
 |-  _I
7 1 6 cdif 
 |-  ( _V \ _I )
8 c2nd 
 |-  2nd
9 7 8 ccom 
 |-  ( ( _V \ _I ) o. 2nd )
10 5 9 ctxp 
 |-  ( 1st (x) ( ( _V \ _I ) o. 2nd ) )
11 4 ccnv 
 |-  `' _E
12 10 11 ccom 
 |-  ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E )
13 4 12 ccom 
 |-  ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
14 13 cfix 
 |-  Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
15 3 14 cdif 
 |-  ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )
16 0 15 wceq 
 |-  Funs = ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )