This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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