Theorem suceldifsn0

Description: A successor that is a member of a set is also a member of that set with the empty set removed. (Contributed by BTernaryTau, 19-Oct-2026)

	Ref	Expression
Hypotheses	suceldifsn0.1	⊢ 𝐴 ∈ 𝐵
	suceldifsn0.2	⊢ 𝐴 = suc 𝐶
Assertion	suceldifsn0	⊢ 𝐴 ∈ ( 𝐵 ∖ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		suceldifsn0.1	⊢ 𝐴 ∈ 𝐵
2		suceldifsn0.2	⊢ 𝐴 = suc 𝐶
3		nsuceq0	⊢ suc 𝐶 ≠ ∅
4	2 3	eqnetri	⊢ 𝐴 ≠ ∅
5		eldifsn	⊢ ( 𝐴 ∈ ( 𝐵 ∖ { ∅ } ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) )
6	1 4 5	mpbir2an	⊢ 𝐴 ∈ ( 𝐵 ∖ { ∅ } )