NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sneq Structured version   Unicode version

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

Proof of Theorem sneq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2362 . . 3
21abbidv 2467 . 2
3 df-sn 3741 . 2
4 df-sn 3741 . 2
52, 3, 43eqtr4g 2410 1
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1642  cab 2339  csn 3737
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  4413  nnsucelr  4427  eqtfinrelk  4486  nnadjoin  4520  elimapw12  4959  elimapw13  4960  elimapw11c  4962  elxp4  5141  fnunsn  5227  fconstg  5289  f1osng  5363  fsng  5473  fnressn  5478  fressnfv  5479  funsex  5856  transex  5930  refex  5931  foundex  5934  extex  5935  eceq1  5982  xpsneng  6071  enadj  6080  enpw1lem1  6081  enpw1  6082  enmap2lem1  6083  enmap1lem1  6089  nenpw1pwlem2  6105  1cnc  6160  df1c3g  6162  spacval  6282  nchoicelem11  6299  nchoicelem16  6304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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
  Copyright terms: Public domain W3C validator