Theorem sneq 3604

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sneq	|- ( A = B -> { A } = { B } )

Proof of Theorem sneq

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2187	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2295	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3599	. 2 |- { A } = { x | x = A }
4		df-sn 3599	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2235	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1353   {cab 2163   {csn 3593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-sn 3599

This theorem is referenced by:  sneqi  3605  sneqd  3606  euabsn  3663  absneu  3665  preq1  3670  tpeq3  3681  snssgOLD  3729  sneqrg  3763  sneqbg  3764  opeq1  3779  unisng  3827  exmidsssn  4203  exmidsssnc  4204  suceq  4403  snnex  4449  opeliunxp  4682  relop  4778  elimasng  4997  dmsnsnsng  5107  elxp4  5117  elxp5  5118  iotajust  5178  fconstg  5413  f1osng  5503  nfvres  5549  fsng  5690  fnressn  5703  fressnfv  5704  funfvima3  5751  isoselem  5821  1stvalg  6143  2ndvalg  6144  2ndval2  6157  fo1st  6158  fo2nd  6159  f1stres  6160  f2ndres  6161  mpomptsx  6198  dmmpossx  6200  fmpox  6201  brtpos2  6252  dftpos4  6264  tpostpos  6265  eceq1  6570  fvdiagfn  6693  mapsncnv  6695  elixpsn  6735  ixpsnf1o  6736  ensn1g  6797  en1  6799  xpsneng  6822  xpcomco  6826  xpassen  6830  xpdom2  6831  phplem3  6854  phplem3g  6856  fidifsnen  6870  xpfi  6929  pm54.43  7189  cc2lem  7265  cc2  7266  exp3val  10522  fsum2dlemstep  11442  fsumcnv  11445  fisumcom2  11446  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  txswaphmeolem  13823