Metamath Proof Explorer

Theorem sucunisn

Description: The successor to the union of any singleton of a set is the successor of the set. (Contributed by RP, 11-Feb-2025)

Ref Expression
Assertion sucunisn 
|- ( A e. V -> suc U. { A } = suc A )

Proof

Step Hyp Ref Expression
1 unisng 
 |-  ( A e. V -> U. { A } = A )
2 suceq 
 |-  ( U. { A } = A -> suc U. { A } = suc A )
3 1 2 syl 
 |-  ( A e. V -> suc U. { A } = suc A )