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

Theorem sneqi 4021
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 4020 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2ax-mp 5 1  |-  { A }  =  { B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381   {csn 4010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-sn 4011
This theorem is referenced by:  fnressn  6064  fressnfv  6066  snriota  6268  xpassen  7609  ids1  12583  strlemor1  14596  strle1  14600  ghmeqker  16162  pws1  17133  pwsmgp  17135  lpival  17761  mat1dimelbas  18840  mat1dim0  18842  mat1dimid  18843  mat1dimscm  18844  mat1dimmul  18845  mat1f1o  18847  imasdsf1olem  20742  vdgr1c  24770  ginvsn  25216  zrdivrng  25299  hh0oi  26687  eulerpartlemmf  28180  dffv5  29542  bpoly3  29788  isdrngo1  30327  mapfzcons  30616  mapfzcons1  30617  mapfzcons2  30619  fourierdlem80  31854  lmod1zr  32804  bnj601  33685
  Copyright terms: Public domain W3C validator