Theorem sneq 3644

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 2215	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2323	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3639	. 2 |- { A } = { x | x = A }
4		df-sn 3639	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2263	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1373   {cab 2191   {csn 3633

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-sn 3639

This theorem is referenced by:  sneqi  3645  sneqd  3646  euabsn  3703  absneu  3705  preq1  3710  tpeq3  3721  snssgOLD  3769  sneqrg  3803  sneqbg  3804  opeq1  3819  unisng  3867  exmidsssn  4246  exmidsssnc  4247  suceq  4449  snnex  4495  opeliunxp  4730  relop  4828  elimasng  5050  dmsnsnsng  5160  elxp4  5170  elxp5  5171  iotajust  5231  fconstg  5472  f1osng  5563  nfvres  5610  fsng  5753  funopsn  5762  fnressn  5770  fressnfv  5771  funfvima3  5818  isoselem  5889  1stvalg  6228  2ndvalg  6229  2ndval2  6242  fo1st  6243  fo2nd  6244  f1stres  6245  f2ndres  6246  mpomptsx  6283  dmmpossx  6285  fmpox  6286  brtpos2  6337  dftpos4  6349  tpostpos  6350  eceq1  6655  fvdiagfn  6780  mapsncnv  6782  elixpsn  6822  ixpsnf1o  6823  ensn1g  6889  en1  6891  xpsneng  6917  xpcomco  6921  xpassen  6925  xpdom2  6926  phplem3  6951  phplem3g  6953  fidifsnen  6967  xpfi  7029  pm54.43  7298  cc2lem  7378  cc2  7379  exp3val  10686  fsum2dlemstep  11745  fsumcnv  11748  fisumcom2  11749  fprod2dlemstep  11933  fprodcnv  11936  fprodcom2fi  11937  pwsval  13123  lssats2  14176  lspsneq0  14188  txswaphmeolem  14792