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 𝐴 ∈ V
Assertion sucidALT 𝐴 ∈ suc 𝐴

Proof

Step Hyp Ref Expression
1 sucidALT.1 𝐴 ∈ V
2 1 snid 𝐴 ∈ { 𝐴 }
3 elun1 ( 𝐴 ∈ { 𝐴 } → 𝐴 ∈ ( { 𝐴 } ∪ 𝐴 ) )
4 2 3 ax-mp 𝐴 ∈ ( { 𝐴 } ∪ 𝐴 )
5 df-suc suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
6 5 equncomi suc 𝐴 = ( { 𝐴 } ∪ 𝐴 )
7 4 6 eleqtrri 𝐴 ∈ suc 𝐴