Metamath Proof Explorer

Theorem r1sssucd

Description: Deductive form of r1sssuc . (Contributed by Noam Pasman, 19-Jan-2025)

Ref Expression
Hypothesis r1sssucd.1 
|- ( ph -> A e. On )
Assertion r1sssucd 
|- ( ph -> ( R1 ` A ) C_ ( R1 ` suc A ) )

Proof

Step Hyp Ref Expression
1 r1sssucd.1 
 |-  ( ph -> A e. On )
2 r1sssuc 
 |-  ( A e. On -> ( R1 ` A ) C_ ( R1 ` suc A ) )
3 1 2 syl 
 |-  ( ph -> ( R1 ` A ) C_ ( R1 ` suc A ) )