Metamath Proof Explorer

Theorem sucel

Description: Membership of a successor in another class. (Contributed by NM, 29-Jun-2004)

Ref Expression
Assertion sucel ⊢ suc ⁡ A ∈ B ↔ ∃ x ∈ B ∀ y y ∈ x ↔ y ∈ A ∨ y = A

Proof

Step Hyp Ref Expression
1 risset ⊢ suc ⁡ A ∈ B ↔ ∃ x ∈ B x = suc ⁡ A
2 dfcleq ⊢ x = suc ⁡ A ↔ ∀ y y ∈ x ↔ y ∈ suc ⁡ A
3 vex ⊢ y ∈ V
4 3 elsuc ⊢ y ∈ suc ⁡ A ↔ y ∈ A ∨ y = A
5 4 bibi2i ⊢ y ∈ x ↔ y ∈ suc ⁡ A ↔ y ∈ x ↔ y ∈ A ∨ y = A
6 5 albii ⊢ ∀ y y ∈ x ↔ y ∈ suc ⁡ A ↔ ∀ y y ∈ x ↔ y ∈ A ∨ y = A
7 2 6 bitri ⊢ x = suc ⁡ A ↔ ∀ y y ∈ x ↔ y ∈ A ∨ y = A
8 7 rexbii ⊢ ∃ x ∈ B x = suc ⁡ A ↔ ∃ x ∈ B ∀ y y ∈ x ↔ y ∈ A ∨ y = A
9 1 8 bitri ⊢ suc ⁡ A ∈ B ↔ ∃ x ∈ B ∀ y y ∈ x ↔ y ∈ A ∨ y = A