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

Metamath Proof Explorer

Theorem iseven2

Description: The predicate "is an even number". An even number is an integer which is divisible by 2. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion iseven2 ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ 2 ∥ Z

Proof

Step Hyp Ref Expression
1 breq2 ⊢ z = Z → 2 ∥ z ↔ 2 ∥ Z
2 dfeven2 ⊢ Even = z ∈ ℤ | 2 ∥ z
3 1 2 elrab2 ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ 2 ∥ Z