Metamath Proof Explorer

Theorem sneqi

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

Ref Expression
Hypothesis sneqi.1 
|- A = B
Assertion sneqi 
|- { A } = { B }

Proof

Step Hyp Ref Expression
1 sneqi.1 
 |-  A = B
2 sneq 
 |-  ( A = B -> { A } = { B } )
3 1 2 ax-mp 
 |-  { A } = { B }