Theorem sneq 3744

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 2362	. . 3 ⊢ (A = B → (x = A ↔ x = B))
2	1	abbidv 2467	. 2 ⊢ (A = B → {x ∣ x = A} = {x ∣ x = B})
3		df-sn 3741	. 2 ⊢ {A} = {x ∣ x = A}
4		df-sn 3741	. 2 ⊢ {B} = {x ∣ x = B}
5	2, 3, 4	3eqtr4g 2410	1 ⊢ (A = B → {A} = {B})

Syntax hints:   → wi 4   = wceq 1642  {cab 2339  {csn 3737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-sn 3741

This theorem is referenced by:  sneqi  3745  sneqd  3746  euabsn  3792  absneu  3794  preq1  3799  tpeq3  3810  snssg  3844  sneqrg  3874  sneqbg  3875  unsneqsn  3887  unisng  3908  opkeq1  4059  snex  4111  snel1c  4140  snel1cg  4141  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  pw1sn  4165  eluni1g  4172  elp6  4263  dfpw12  4301  eqpw1uni  4330  pw1eqadj  4332  iotajust  4338  elsuci  4414  nnsucelr  4428  eqtfinrelk  4486  nnadjoin  4520  opeliunxp  4820  elimapw12  4945  elimapw13  4946  elimapw11c  4948  elxp4  5108  fnunsn  5190  fconstg  5251  f1osng  5323  fsng  5433  fnressn  5438  fressnfv  5439  fmpt2x  5730  funsex  5828  eceq1  5962  xpsneng  6050  enadj  6060  enpw1lem1  6061  enpw1  6062  nenpw1pwlem2  6085  1cnc  6139  df1c3g  6141  nmembers1lem3  6270  spacval  6282  nchoicelem11  6299  nchoicelem16  6304  frecxp  6314