Description: Alternate proof of nnex , more direct, that makes use of ax-rep . (Contributed by Mario Carneiro, 3-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nnexALT | |- NN e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nn | |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) |
|
| 2 | rdgfun | |- Fun rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |
|
| 3 | omex | |- _om e. _V |
|
| 4 | funimaexg | |- ( ( Fun rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) /\ _om e. _V ) -> ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) e. _V ) |
|
| 5 | 2 3 4 | mp2an | |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) e. _V |
| 6 | 1 5 | eqeltri | |- NN e. _V |