Theorem sneq 3629

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sneq	⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Proof of Theorem sneq

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2203	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2311	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 3624	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 3624	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2251	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1364  {cab 2179  {csn 3618

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-sn 3624

This theorem is referenced by:  sneqi  3630  sneqd  3631  euabsn  3688  absneu  3690  preq1  3695  tpeq3  3706  snssgOLD  3754  sneqrg  3788  sneqbg  3789  opeq1  3804  unisng  3852  exmidsssn  4231  exmidsssnc  4232  suceq  4433  snnex  4479  opeliunxp  4714  relop  4812  elimasng  5033  dmsnsnsng  5143  elxp4  5153  elxp5  5154  iotajust  5214  fconstg  5450  f1osng  5541  nfvres  5588  fsng  5731  fnressn  5744  fressnfv  5745  funfvima3  5792  isoselem  5863  1stvalg  6195  2ndvalg  6196  2ndval2  6209  fo1st  6210  fo2nd  6211  f1stres  6212  f2ndres  6213  mpomptsx  6250  dmmpossx  6252  fmpox  6253  brtpos2  6304  dftpos4  6316  tpostpos  6317  eceq1  6622  fvdiagfn  6747  mapsncnv  6749  elixpsn  6789  ixpsnf1o  6790  ensn1g  6851  en1  6853  xpsneng  6876  xpcomco  6880  xpassen  6884  xpdom2  6885  phplem3  6910  phplem3g  6912  fidifsnen  6926  xpfi  6986  pm54.43  7250  cc2lem  7326  cc2  7327  exp3val  10612  fsum2dlemstep  11577  fsumcnv  11580  fisumcom2  11581  fprod2dlemstep  11765  fprodcnv  11768  fprodcom2fi  11769  lssats2  13910  lspsneq0  13922  txswaphmeolem  14488