Metamath Proof Explorer

Theorem elsucg

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

Ref Expression
Assertion elsucg ⊢ A ∈ V → A ∈ suc ⁡ B ↔ A ∈ B ∨ A = B

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc ⁡ B = B ∪ B
2 1 eleq2i ⊢ A ∈ suc ⁡ B ↔ A ∈ B ∪ B
3 elun ⊢ A ∈ B ∪ B ↔ A ∈ B ∨ A ∈ B
4 2 3 bitri ⊢ A ∈ suc ⁡ B ↔ A ∈ B ∨ A ∈ B
5 elsng ⊢ A ∈ V → A ∈ B ↔ A = B
6 5 orbi2d ⊢ A ∈ V → A ∈ B ∨ A ∈ B ↔ A ∈ B ∨ A = B
7 4 6 bitrid ⊢ A ∈ V → A ∈ suc ⁡ B ↔ A ∈ B ∨ A = B