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

Metamath Proof Explorer

Theorem sucidALT

Description: A set belongs to its successor. This proof was automatically derived from sucidALTVD using translate__without__overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sucidALT.1 ⊢ A ∈ V
Assertion sucidALT ⊢ A ∈ suc ⁡ A

Proof

Step Hyp Ref Expression
1 sucidALT.1 ⊢ A ∈ V
2 1 snid ⊢ A ∈ A
3 elun1 ⊢ A ∈ A → A ∈ A ∪ A
4 2 3 ax-mp ⊢ A ∈ A ∪ A
5 df-suc ⊢ suc ⁡ A = A ∪ A
6 5 equncomi ⊢ suc ⁡ A = A ∪ A
7 4 6 eleqtrri ⊢ A ∈ suc ⁡ A