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	⊢ ℤ ∈ V

Proof

Step	Hyp	Ref	Expression
1		dfz2	⊢ ℤ = ( − “ ( ℕ × ℕ ) )
2		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
3		ffun	⊢ ( − : ( ℂ × ℂ ) ⟶ ℂ → Fun − )
4		nnexALT	⊢ ℕ ∈ V
5	4 4	xpex	⊢ ( ℕ × ℕ ) ∈ V
6	5	funimaex	⊢ ( Fun − → ( − “ ( ℕ × ℕ ) ) ∈ V )
7	2 3 6	mp2b	⊢ ( − “ ( ℕ × ℕ ) ) ∈ V
8	1 7	eqeltri	⊢ ℤ ∈ V