Theorem sneq 2475

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15.

Assertion

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

Proof of Theorem sneq

Step	Hyp	Ref	Expression
1		eqeq2 1527	. . 3 |- (A = B -> (x = A <-> x = B))
2	1	abbidv 1620	. 2 |- (A = B -> {x | x = A} = {x | x = B})
3		df-sn 2470	. 2 |- {A} = {x | x = A}
4		df-sn 2470	. 2 |- {B} = {x | x = B}
5	2, 3, 4	3eqtr4g 1574	1 |- (A = B -> {A} = {B})

Syntax hints:   -> wi 3   = wceq 992  {cab 1505  {csn 2467

This theorem is referenced by:  sneqi 2476  sneqd 2477  eusn 2507  preq1 2509  snssg 2527  opeq1 2552  unisng 2585  snex 2826  opthwiener 2884  suceq 3038  snnex 3100  reusn 3115  reusni 3116  relop 3365  elimasng 3519  eliniseg 3521  dmsnop 3577  elxp4 3585  elxp5 3586  fconstg 3766  fveq2 3835  fnressn 3951  fressnfv 3952  funfvima3 3968  isofrlem 4015  1stval 4142  2ndval 4143  2ndval2 4151  fo1st 4152  fo2nd 4153  f1stres 4154  f2ndres 4155  tfrlem10 4221  eceq2 4418  ensn1g 4566  en1 4567  xpsneng 4577  xpcomen 4580  xpassen 4582  xpdom2 4583  canth2 4629  xpmapenlem2 4644  xpmapenlem5 4647  mapunen 4649  phplem3 4657  pm54.43 4715  aceq5lem3 4883  aceq5lem4 4884  kmlem9 4919  kmlem11 4921  kmlem12 4922  cardsn 4982  snunioo 6542  expval 6765  xpnnen 7711  islp 7954  gxval 8314  h1de2ctlem 9754  spansn 9758  elspansn 9765  elspansn2 9766  spansneleq 9769  h1datom 9781  spansnj 9870  spansncv 9876  superpos 10562  sumdmdlem2 10628  moec 10745  on1el3 10962  osneisi 11018  plimfil 11103  locfinnei 11573  neibastop3 11585  ist1-2 11603  ist1-3 11604  t1sncld 11606  isfillim 11676  hausfillim 11685  filmapf 11688  dif1en 11833  fimax 11837  fixp 11840  inficl 11849  tlmbr 11965  ismrer1 12080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-sn 2470

Copyright terms: Public domain