Theorem sneq 3745

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 2468	. 2 ⊢ (A = B → {x ∣ x = A} = {x ∣ x = B})
3		df-sn 3742	. 2 ⊢ {A} = {x ∣ x = A}
4		df-sn 3742	. 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 3738

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 3742

This theorem is referenced by:  sneqi  3746  sneqd  3747  euabsn  3793  absneu  3795  preq1  3800  tpeq3  3811  snssg  3845  sneqrg  3875  sneqbg  3876  unsneqsn  3888  unisng  3909  opkeq1  4060  snex  4112  snel1c  4141  snel1cg  4142  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  pw1sn  4166  eluni1g  4173  elp6  4264  dfpw12  4302  eqpw1uni  4331  pw1eqadj  4333  iotajust  4339  elsuci  4415  nnsucelr  4429  eqtfinrelk  4487  nnadjoin  4521  opeliunxp  4821  elimapw12  4946  elimapw13  4947  elimapw11c  4949  elxp4  5109  fnunsn  5191  fconstg  5252  f1osng  5324  fsng  5434  fnressn  5439  fressnfv  5440  fmpt2x  5731  funsex  5829  eceq1  5963  xpsneng  6051  enadj  6061  enpw1lem1  6062  enpw1  6063  nenpw1pwlem2  6086  1cnc  6140  df1c3g  6142  nmembers1lem3  6271  spacval  6283  nchoicelem11  6300  nchoicelem16  6305  frecxp  6315