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 )