Theorem zexALT

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	$$⊢\mathbb{Z}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfz2	$$⊢\mathbb{Z}=-\left[\mathbb{N}\times \mathbb{N}\right]$$
2		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
3		ffun	$$⊢-:ℂ\times ℂ⟶ℂ\to \mathrm{Fun}-$$
4		nnexALT	$$⊢\mathbb{N}\in \mathrm{V}$$
5	4 4	xpex	$$⊢\mathbb{N}\times \mathbb{N}\in \mathrm{V}$$
6	5	funimaex	$$⊢\mathrm{Fun}-\to -\left[\mathbb{N}\times \mathbb{N}\right]\in \mathrm{V}$$
7	2 3 6	mp2b	$$⊢-\left[\mathbb{N}\times \mathbb{N}\right]\in \mathrm{V}$$
8	1 7	eqeltri	$$⊢\mathbb{Z}\in \mathrm{V}$$