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	⊢ 𝐴 ∈ On
Assertion	onuniorsuciOLD	⊢ ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		onssi.1	⊢ 𝐴 ∈ On
2		onuniorsuc	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
3	1 2	ax-mp	⊢ ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 )