MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sneqi Structured version   Unicode version

Theorem sneqi 4031
Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqi.1  |-  A  =  B
Assertion
Ref Expression
sneqi  |-  { A }  =  { B }

Proof of Theorem sneqi
StepHypRef Expression
1 sneqi.1 . 2  |-  A  =  B
2 sneq 4030 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2ax-mp 5 1  |-  { A }  =  { B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374   {csn 4020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-sn 4021
This theorem is referenced by:  fnressn  6064  fressnfv  6066  snriota  6266  xpassen  7601  ids1  12560  strlemor1  14571  strle1  14575  ghmeqker  16081  pws1  17042  pwsmgp  17044  lpival  17668  mat1dimelbas  18733  mat1dim0  18735  mat1dimid  18736  mat1dimscm  18737  mat1dimmul  18738  mat1f1o  18740  imasdsf1olem  20604  vdgr1c  24567  ginvsn  25013  zrdivrng  25096  hh0oi  26484  eulerpartlemmf  27940  dffv5  29137  bpoly3  29383  isdrngo1  29949  mapfzcons  30239  mapfzcons1  30240  mapfzcons2  30242  fourierdlem80  31442  lmod1zr  32050  bnj601  32932
  Copyright terms: Public domain W3C validator