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	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ suc 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	⊢ suc 𝐵 = ( 𝐵 ∪ { 𝐵 } )
2	1	eleq2i	⊢ ( 𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ ( 𝐵 ∪ { 𝐵 } ) )
3		elun	⊢ ( 𝐴 ∈ ( 𝐵 ∪ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐵 } ) )
4		elsn2g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )
5	4	orbi2d	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 ∈ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
6	3 5	bitrid	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( 𝐵 ∪ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
7	2 6	bitrid	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ suc 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )