Theorem elsuci

Description: Membership in a successor. This one-way implication does not require that either A or B be sets. (Contributed by NM, 6-Jun-1994)

	Ref	Expression
Assertion	elsuci	⊢ ( 𝐴 ∈ suc 𝐵 → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	⊢ suc 𝐵 = ( 𝐵 ∪ { 𝐵 } )
2	1	eleq2i	⊢ ( 𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ ( 𝐵 ∪ { 𝐵 } ) )
3		elun	⊢ ( 𝐴 ∈ ( 𝐵 ∪ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐵 } ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ suc 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐵 } ) )
5		elsni	⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )
6	5	orim2i	⊢ ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐵 } ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) )
7	4 6	sylbi	⊢ ( 𝐴 ∈ suc 𝐵 → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) )