Metamath Proof Explorer

Theorem wlimeq1

Description: Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018)

Ref Expression
Assertion wlimeq1 
|- ( R = S -> WLim ( R , A ) = WLim ( S , A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 wlimeq12 
 |-  ( ( R = S /\ A = A ) -> WLim ( R , A ) = WLim ( S , A ) )
3 1 2 mpan2 
 |-  ( R = S -> WLim ( R , A ) = WLim ( S , A ) )