Metamath Proof Explorer


Theorem sucexb

Description: A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998)

Ref Expression
Assertion sucexb ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V )

Proof

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 )