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

Metamath Proof Explorer

Theorem sucexb

Description: A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998)

Ref Expression
Assertion sucexb ⊢ A ∈ V ↔ suc ⁡ A ∈ V

Proof

Step Hyp Ref Expression
1 unexb ⊢ A ∈ V ∧ A ∈ V ↔ A ∪ A ∈ V
2 snex ⊢ A ∈ V
3 2 biantru ⊢ A ∈ V ↔ A ∈ V ∧ A ∈ V
4 df-suc ⊢ suc ⁡ A = A ∪ A
5 4 eleq1i ⊢ suc ⁡ A ∈ V ↔ A ∪ A ∈ V
6 1 3 5 3bitr4i ⊢ A ∈ V ↔ suc ⁡ A ∈ V