Description: Alternate proof of zex . (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 16-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | zexALT | |- ZZ e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfz2 | |- ZZ = ( - " ( NN X. NN ) ) |
|
| 2 | subf | |- - : ( CC X. CC ) --> CC |
|
| 3 | ffun | |- ( - : ( CC X. CC ) --> CC -> Fun - ) |
|
| 4 | nnexALT | |- NN e. _V |
|
| 5 | 4 4 | xpex | |- ( NN X. NN ) e. _V |
| 6 | 5 | funimaex | |- ( Fun - -> ( - " ( NN X. NN ) ) e. _V ) |
| 7 | 2 3 6 | mp2b | |- ( - " ( NN X. NN ) ) e. _V |
| 8 | 1 7 | eqeltri | |- ZZ e. _V |