Metamath Proof Explorer

Theorem sneqd

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004)

Ref Expression
Hypothesis sneqd.1 
|- ( ph -> A = B )
Assertion sneqd 
|- ( ph -> { A } = { B } )

Proof

Step Hyp Ref Expression
1 sneqd.1 
 |-  ( ph -> A = B )
2 sneq 
 |-  ( A = B -> { A } = { B } )
3 1 2 syl 
 |-  ( ph -> { A } = { B } )