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

Theorem sneqi 3828
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 3827 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2ax-mp 8 1  |-  { A }  =  { B }
Colors of variables: wff set class
Syntax hints:    = wceq 1653   {csn 3816
This theorem is referenced by:  fnressn  5920  fressnfv  5922  xpassen  7204  ids1  11753  strlemor1  13558  strle1  13562  ghmeqker  15034  pws1  15724  pwsmgp  15726  lpival  16318  imasdsf1olem  18405  vdgr1c  21678  ginvsn  21939  zrdivrng  22022  hh0oi  23408  dffv5  25771  bpoly3  26106  isdrngo1  26574  mapfzcons  26774  mapfzcons1  26775  mapfzcons2  26777  bnj601  29353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-sn 3822
  Copyright terms: Public domain W3C validator