Metamath Proof Explorer

Theorem wlimeq2

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

Ref Expression
Assertion wlimeq2 
|- ( A = B -> WLim ( R , A ) = WLim ( R , B ) )

Proof

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