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	$$⊢A\in \mathrm{On}$$
Assertion	onuniorsuciOLD	$$⊢\left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$

Proof

Step	Hyp	Ref	Expression
1		onssi.1	$$⊢A\in \mathrm{On}$$
2		onuniorsuc	$$⊢A\in \mathrm{On}\to \left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$
3	1 2	ax-mp	$$⊢\left(A=\bigcup A\vee A=\mathrm{suc}\bigcup A\right)$$