Description: A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | sucexb | ⊢ ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unexb | ⊢ ( ( 𝐴 ∈ V ∧ { 𝐴 } ∈ V ) ↔ ( 𝐴 ∪ { 𝐴 } ) ∈ V ) | |
2 | snex | ⊢ { 𝐴 } ∈ V | |
3 | 2 | biantru | ⊢ ( 𝐴 ∈ V ↔ ( 𝐴 ∈ V ∧ { 𝐴 } ∈ V ) ) |
4 | df-suc | ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) | |
5 | 4 | eleq1i | ⊢ ( suc 𝐴 ∈ V ↔ ( 𝐴 ∪ { 𝐴 } ) ∈ V ) |
6 | 1 3 5 | 3bitr4i | ⊢ ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V ) |