Metamath Proof Explorer

Theorem eqelsuc

Description: A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994)

Ref Expression
Hypothesis eqelsuc.1 
|- A e. _V
Assertion eqelsuc 
|- ( A = B -> A e. suc B )

Proof

Step Hyp Ref Expression
1 eqelsuc.1 
 |-  A e. _V
2 1 sucid 
 |-  A e. suc A
3 suceq 
 |-  ( A = B -> suc A = suc B )
4 2 3 eleqtrid 
 |-  ( A = B -> A e. suc B )