Description: A set belongs to its successor. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools
program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant.
sucid is sucidVD without virtual deductions and was automatically
derived from sucidVD .
h1::
|- A e. _V
2:1:
|- A e. { A }
3:2:
|- A e. ( A u. { A } )
4::
|- suc A = ( A u. { A } )
qed:3,4:
|- A e. suc A
(Contributed by Alan Sare, 18-Feb-2012) (Proof modification is
discouraged.) (New usage is discouraged.)