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 AV
Assertion sucidALT AsucA

Proof

Step Hyp Ref Expression
1 sucidALT.1 AV
2 1 snid AA
3 elun1 AAAAA
4 2 3 ax-mp AAA
5 df-suc sucA=AA
6 5 equncomi sucA=AA
7 4 6 eleqtrri AsucA