Description: Although CC can be proven trivially using ac5 , we prove it here using DC. (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | axcc | |- ( x ~~ _om -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- ( x \ { (/) } ) = ( x \ { (/) } ) |
|
2 | eqid | |- ( t e. _om , y e. U. ( x \ { (/) } ) |-> ( v ` t ) ) = ( t e. _om , y e. U. ( x \ { (/) } ) |-> ( v ` t ) ) |
|
3 | eqid | |- ( w e. ( x \ { (/) } ) |-> ( u ` suc ( `' v ` w ) ) ) = ( w e. ( x \ { (/) } ) |-> ( u ` suc ( `' v ` w ) ) ) |
|
4 | 1 2 3 | axcclem | |- ( x ~~ _om -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |