Theorem sneq 3603

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 3598	. 2 |- { A } = { x | x = A }
4		df-sn 3598	. 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 3592

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 3598

This theorem is referenced by:  sneqi  3604  sneqd  3605  euabsn  3662  absneu  3664  preq1  3669  tpeq3  3680  snssgOLD  3728  sneqrg  3762  sneqbg  3763  opeq1  3778  unisng  3826  exmidsssn  4202  exmidsssnc  4203  suceq  4402  snnex  4448  opeliunxp  4681  relop  4777  elimasng  4996  dmsnsnsng  5106  elxp4  5116  elxp5  5117  iotajust  5177  fconstg  5412  f1osng  5502  nfvres  5548  fsng  5689  fnressn  5702  fressnfv  5703  funfvima3  5750  isoselem  5820  1stvalg  6142  2ndvalg  6143  2ndval2  6156  fo1st  6157  fo2nd  6158  f1stres  6159  f2ndres  6160  mpomptsx  6197  dmmpossx  6199  fmpox  6200  brtpos2  6251  dftpos4  6263  tpostpos  6264  eceq1  6569  fvdiagfn  6692  mapsncnv  6694  elixpsn  6734  ixpsnf1o  6735  ensn1g  6796  en1  6798  xpsneng  6821  xpcomco  6825  xpassen  6829  xpdom2  6830  phplem3  6853  phplem3g  6855  fidifsnen  6869  xpfi  6928  pm54.43  7188  cc2lem  7264  cc2  7265  exp3val  10521  fsum2dlemstep  11441  fsumcnv  11444  fisumcom2  11445  fprod2dlemstep  11629  fprodcnv  11632  fprodcom2fi  11633  txswaphmeolem  13790