Metamath Proof Explorer


Theorem onuniorsuciOLD

Description: Obsolete version of onuniorsuc as of 11-Jan-2025. (Contributed by NM, 13-Jun-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis onssi.1 AOn
Assertion onuniorsuciOLD A=AA=sucA

Proof

Step Hyp Ref Expression
1 onssi.1 AOn
2 onuniorsuc AOnA=AA=sucA
3 1 2 ax-mp A=AA=sucA