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	$$⊢A\in \mathrm{suc}B\to \left(A\in B\vee A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-suc	$$⊢\mathrm{suc}B=B\cup \left\{B\right\}$$
2	1	eleq2i	$$⊢A\in \mathrm{suc}B\leftrightarrow A\in \left(B\cup \left\{B\right\}\right)$$
3		elun	$$⊢A\in \left(B\cup \left\{B\right\}\right)\leftrightarrow \left(A\in B\vee A\in \left\{B\right\}\right)$$
4	2 3	bitri	$$⊢A\in \mathrm{suc}B\leftrightarrow \left(A\in B\vee A\in \left\{B\right\}\right)$$
5		elsni	$$⊢A\in \left\{B\right\}\to A=B$$
6	5	orim2i	$$⊢\left(A\in B\vee A\in \left\{B\right\}\right)\to \left(A\in B\vee A=B\right)$$
7	4 6	sylbi	$$⊢A\in \mathrm{suc}B\to \left(A\in B\vee A=B\right)$$