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