Theorem elsucg

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

	Ref	Expression
Assertion	elsucg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ suc 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )

Proof

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