Theorem elsuc2g

Description: Variant of membership in a successor, requiring that B rather than A be a set. (Contributed by NM, 28-Oct-2003)

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