Theorem elsucg

Description: Membership in a successor. Exercise 5 of TakeutiZaring p. 17. (Contributed by NM, 15-Sep-1995)

	Ref	Expression
Assertion	elsucg	$$⊢A\in V\to \left(A\in \mathrm{suc}B\leftrightarrow \left(A\in B\vee A=B\right)\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		elsng	$$⊢A\in V\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
6	5	orbi2d	$$⊢A\in V\to \left(\left(A\in B\vee A\in \left\{B\right\}\right)\leftrightarrow \left(A\in B\vee A=B\right)\right)$$
7	4 6	bitrid	$$⊢A\in V\to \left(A\in \mathrm{suc}B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$