Theorem elelsuc

Description: Membership in a successor. (Contributed by NM, 20-Jun-1998)

	Ref	Expression
Assertion	elelsuc	$$⊢A\in B\to A\in \mathrm{suc}B$$

Proof

Step	Hyp	Ref	Expression
1		orc	$$⊢A\in B\to \left(A\in B\vee A=B\right)$$
2		elsucg	$$⊢A\in B\to \left(A\in \mathrm{suc}B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$
3	1 2	mpbird	$$⊢A\in B\to A\in \mathrm{suc}B$$