New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sneq | GIF version |
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sneq | ⊢ (A = B → {A} = {B}) |
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}) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |