forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathchanges-set.txt
13298 lines (13292 loc) · 636 KB
/
changes-set.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Recent label changes
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
This is part of an ongoing project to improve naming consistency. If you have
suggestions for better names, let us know. It lists changes in set.mm (for
iset.mm, see the git history, although many of the proposed or historical
changes described here also apply to iset.mm, or should be adopted in iset.mm
when someone gets the chance).
To update your mathbox, you can make global substitutions into
your local version by processing the ones WITHOUT "Notes" in REVERSE order.
The ones WITH "Notes" may have to be processed manually.
PROPOSED:
Date Old New Notes
proposed nfiundg nfiund
proposed bnj1441g bnj1441
proposed cbviinvg cbviinv
proposed cbviunvg cbviunv
proposed cbviing cbviin
proposed cbviung cbviun
proposed nfiing nfiin
proposed nfiung nfiun
proposed nfaba1g nfaba1
proposed nfabg nfab
proposed hblemg hblem
proposed nfsabg nfsab
proposed hbabg hbab
proposed cbvmptvg cbvmptv
proposed cbvmptg cbvmpt
proposed cbvmptfg cbvmptf
proposed cbvopab1g cbvopab1
proposed nfiund nfiundv
proposed bnj1441 bnj1441v
proposed cbviinv cbviinvv
proposed cbviunv cbviunvv
proposed cbviin cbviinv
proposed cbviun cbviunv
proposed nfiin nfiinv
proposed nfiun nfiunv
proposed nfaba1 nfaba1v
proposed nfab nfabv
proposed hblem hblemv
proposed nfsab nfsabv
proposed hbab hbabv
proposed cbvmptv cbvmptvv
proposed cbvmpt cbvmptv
proposed cbvmptf cbvmptfv
proposed cbvopab1 cbvopab1v
proposed syl imtri (analogous to *bitr*, sstri, etc.)
there is less agreement on renaming syl
than others here
proposed syld imtrd
proposed syldc imtrdcom
proposed syldd imtrdd
proposed sylbi biimtri
proposed sylib imbitri
proposed sylbb bitriim
proposed sylibr imbitrri
proposed sylbir biimtrri
proposed sylbbr bitrriim
proposed sylbb1 bitr3iim
proposed sylbb2 bitr4iim
proposed sylibd imbitrd
proposed sylbid biimtrd
proposed sylibrd imbitrrd
proposed sylbird biimtrrd
proposed syl5com imtridcom
proposed syl5 imtrid alternate proposal: sylid
proposed syl56 imtridi
proposed syl5d imtridd
proposed syl5bir biimtrrid
proposed syl5ib imbitrid
proposed syl5ibcom imbitridcom
proposed syl5ibr imbitrrid
proposed syl5ibrcom imbitrridcom
proposed syl6 imtrdi alternate proposal: syldi
proposed syl6com imtrdicom
proposed syl6d imtrdid
proposed syl6ib imbitrdi
proposed syl6ibr imbitrrdi
proposed syl6bi biimtrdi
proposed syl6bir biimtrrdi
(Please send any comments on these proposals to the mailing list or
make a github issue.)
DONE:
Date Old New Notes
10-Jan-25 syl5bi biimtrid
9-Jan-25 fvresval [same] Moved from SF's mathbox to main set.mm
9-Jan-25 brtp [same] Moved from SF's mathbox to main set.mm
9-Jan-25 --- --- Moved initial surreal definitions from
SF's mathbox to main set.mm
9-Jan-25 nfrexdg nfrexd consistent with nfrald
9-Jan-25 nfrexg nfrex consistent with nfral
7-Jan-25 rhmdvdsr [same] Moved from TA's mathbox to main set.mm
7-Jan-25 rhmopp [same] Moved from TA's mathbox to main set.mm
7-Jan-25 elrhmunit [same] Moved from TA's mathbox to main set.mm
7-Jan-25 rhmunitinv [same] Moved from TA's mathbox to main set.mm
7-Jan-25 ringi ringdilem
5-Jan-25 nfrexd nfrexdw consistent with nfraldw
5-Jan-25 nfrex nfrexw consistent with nfralw
4-Jan-25 smorndom smocdmdom
4-Jan-25 ralimda --- obsolete - use ralimdaa instead
3-Jan-25 srgi srgdilem
2-Jan-25 frnnn0fsuppg fcdmnn0fsuppg
2-Jan-25 frnnn0suppg fcdmnn0suppg
2-Jan-25 frnnn0fsupp fcdmnn0fsupp
2-Jan-25 frnnn0supp fcdmnn0supp
2-Jan-25 pr2nelem enpr2
28-Dec-24 fovrnd fovcdmd
28-Dec-24 fovrnda fovcdmda
28-Dec-24 fovrn fovcdm
28-Dec-24 foelrni foelcdmi
28-Dec-24 fornex focdmex
28-Dec-24 fafvelrn fafvelcdm
28-Dec-24 fafv2elrn fafv2elcdm
28-Dec-24 frnvafv2v fcdmafv2v
28-Dec-24 cncffvrn cncfcdm
26-Dec-24 syl5bb bitrid compare to bitri or bitrd
23-Dec-24 sn-iotaex iotaex moved from SN's mathbox to main set.mm
23-Dec-24 sn-iotassuni iotassuni moved from SN's mathbox to main set.mm
23-Dec-24 sn-iotaval iotaval moved from SN's mathbox to main set.mm
23-Dec-24 sn-iotanul iotanul2 moved from SN's mathbox to main set.mm
23-Dec-24 sn-iotauni iotauni2 moved from SN's mathbox to main set.mm
23-Dec-24 iotavallem iotaval2 moved from SN's mathbox to main set.mm
22-Dec-24 frnsuppeq fsuppeq
22-Dec-24 frnsuppeqg fsuppeqg
22-Dec-24 frnfsuppbi ffsuppbi
22-Dec-24 fvmptelrn fvmptelcdm
22-Dec-24 frnssb fcdmssb
19-Dec-24 3albii [same] moved from PM's mathbox to main set.mm
19-Dec-24 ssrel3 [same] moved from PM's mathbox to main set.mm
17-Dec-24 ffvelrnd ffvelcdmd
17-Dec-24 ffvelrnda ffvelcdmda
17-Dec-24 ffvelrni ffvelcdmi
17-Dec-24 ffvelrn ffvelcdm
13-Dec-24 fvmptopab [same] revised - eliminated hypothesis
and deduction form antecedent
13-Dec-24 wksonproplem [same] revised - eliminated hypothesis
13-Dec-24 mptmpoopabovd [same] revised - eliminated hypotheses
13-Dec-24 mptmpoopabbrd [same] revised - eliminated hypotheses
13-Dec-24 wlkRes --- obsolete - use obapresex2 instead
13-Dec-24 opabresex2d --- obsolete - use opabresex2 instead
27-Nov-24 eldifsucnn [same] moved from SF's mathbox to main set.mm
27-Nov-24 nnasmo [same] moved from SF's mathbox to main set.mm
27-Nov-24 rdg0n [same] moved from SF's mathbox to main set.mm
27-Nov-24 dfse3 [same] moved from SF's mathbox to main set.mm
27-Nov-24 3orel3 [same] moved from SF's mathbox to main set.mm
27-Nov-24 3orel2 [same] moved from SF's mathbox to main set.mm
27-Nov-24 --- --- transitive closure theorems moved
from SF's mathbox to main set.mm
25-Nov-24 syl5eq eqtrid
23-Nov-24 leltletr [same] moved from AV's mathbox to main set.mm
23-Nov-24 fzindd [same] moved from metakunt's mathbox to main set.mm
23-Nov-24 elfzop1le2 [same] moved from GS's mathbox to main set.mm
23-Nov-24 elunirn2 [same] moved from TA's mathbox to main set.mm
18-Nov-24 csbcog [same] moved from RP's mathbox to main set.mm
18-Nov-24 csbwrecsg [same] moved from ML's mathbox to main set.mm
18-Nov-24 csbpredg [same] moved from ML's mathbox to main set.mm
18-Nov-24 csbdif [same] moved from ML's mathbox to main set.mm
18-Nov-24 df-wrecs dfwrecsOLD obsoleted
18-Nov-24 dfwrecs2 df-wrecs moved from BJ's mathbox to main set.mm and
made the main definition
16-Nov-24 rspcdvinvd rspcdv2 moved from SP's mathbox to main set.mm
15-Nov-24 baseltedgf basendxltedgfndx
12-Nov-24 sseldi sselid compare to sselii or sseldd
11-Nov-24 mpteq12da [same] moved from GS's mathbox to main set.mm
9-Nov-24 eqsb3 eqsb1
9-Nov-24 eqsbc3 eqsbc1
9-Nov-24 eqsbc3r eqsbc2
9-Nov-24 elsb3 elsb1
9-Nov-24 elsb4 elsb2
9-Nov-24 clelsb3 clelsb1
9-Nov-24 clelsb3fw clelsb1fw
9-Nov-24 clelsb3f clelsb1f
7-Nov-24 slotsbaseefdif basendxnedgfndx
31-Oct-24 ceilged [same] moved from GS's mathbox to main set.mm
31-Oct-24 ceilcld [same] moved from GS's mathbox to main set.mm
31-Oct-24 zexpcld [same] moved from SN's mathbox to main set.mm
28-Oct-24 dfpo2 --- moved from SF's mathbox to main set.mm
27-Oct-24 bnj930 fnfund moved from JB's mathbox to main set.mm
27-Oct-24 predasetex predexg predasetex is deprecated
27-Oct-24 algrflem opco1i
26-Oct-24 fsumsplit1 fsumsplit1 moved from GS's mathbox to main set.mm
26-Oct-24 fsumclf fsumclf moved from GS's mathbox to main set.mm
24-Oct-24 --- --- well-founded recursion theorems moved
from SF's mathbox to main set.mm
22-Oct-24 --- --- well-founded induction theorems moved
from SF's mathbox to main set.mm
20-Oct-24 --- --- transitive predecessor theorems moved
from SF's mathbox to main set.mm
17-Oct-24 posglbd posglbdg compare to poslubdg
16-Oct-24 2ralbiim [same] moved from AV's mathbox to main set.mm
16-Oct-24 --- --- well-founded recursion theorems moved
from SF's mathbox to main set.mm
15-Oct-24 --- --- well-founded induction theorems moved
from SF's mathbox to main set.mm
12-Oct-24 syl5rbb bitr2id compare to bitr2i or bitr2d
10-Oct-24 syl5reqr eqtr3di order of hypotheses is switched
30-Sep-24 syl5req eqtr2id compare to eqtr2i or eqtr2d
27-Sep-24 syldbl2 [same] moved from SP's mathbox to main set.mm
27-Sep-24 fiminre2 [same] moved from GS's mathbox to main set.mm
27-Sep-24 infrefilb [same] moved from GS's mathbox to main set.mm
26-Sep-24 tltnle [same] moved from TA's mathbox to main set.mm
26-Sep-24 tleile [same] moved from TA's mathbox to main set.mm
26-Sep-24 tospos [same] moved from TA's mathbox to main set.mm
25-Sep-24 biadanid [same] moved from TA's mathbox to main set.mm
22-Sep-24 grpcld [same] moved from SN's mathbox to main set.mm
21-Sep-24 sb56 sbalex substitution expressed with 'al' or with 'ex'
21-Sep-24 nanimn dfnan2 mark as an alternative definition
20-Sep-24 fco3 funcofd moved from GS's mathbox to main set.mm
20-Sep-24 freld [same] moved from GS's mathbox to main set.mm
20-Sep-24 ineqcomi [same] moved from PM's mathbox to main set.mm
20-Sep-24 ineqcom [same] moved from PM's mathbox to main set.mm
18-Sep-24 sylibda sylbida moved from SN's mathbox to main set.mm
17-Sep-24 moel [same] moved from TA's mathbox to main set.mm
16-Sep-24 syl5eqr eqtr3id compare to eqtr3i or eqtr3d
14-Sep-24 iunsn [same] moved from SN's mathbox to main set.mm
10-Sep-24 sspreima [same] moved from TA's mathbox to main set.mm
9-Sep-24 syl6bb bitrdi compare to bitri or bitrd
4-Sep-24 bj-df-v dfv2 moved from BJ's mathbox to main set.mm
1-Sep-24 brabsb2 [same] removed unnecessary commutation
1-Sep-24 opelopabsbALT vopelopabsb removed unnecessary commutation
24-Aug-24 dvdspw dvdsexp2im moved from SF's mathbox to main set.mm
24-Aug-24 pdivsq prmdvdssq moved from SF's mathbox to main set.mm
24-Aug-24 dvdstrd [same] moved from MKU's mathbox to main set.mm
23-Aug-24 qred [same] moved from GS's mathbox to main set.mm
21-Aug-24 ralimda [same] moved from GS's mathbox to main set.mm
21-Aug-24 ralrimia [same] moved from GS's mathbox to main set.mm
21-Aug-24 2exp11 [same] moved from AV's mathbox to main set.mm
20-Aug-24 uzssre [same] moved from GS's mathbox to main set.mm
20-Aug-24 unexd [same] moved from SN's mathbox to main set.mm
20-Aug-24 brsnop [same] moved from TA's mathbox to main set.mm
19-Aug-24 dfrp2 [same] moved from TA's mathbox to main set.mm
19-Aug-24 rabeqcda [same] moved from SN's mathbox to main set.mm
18-Aug-24 prdsco [same] revised - compatibility with new df-prds
18-Aug-24 prdshom [same] revised - compatibility with new df-prds
18-Aug-24 prdstset [same] revised - compatibility with new df-prds
18-Aug-24 prdsds [same] revised - compatibility with new df-prds
18-Aug-24 prdsle [same] revised - compatibility with new df-prds
18-Aug-24 prdsip [same] revised - compatibility with new df-prds
18-Aug-24 prdsvsca [same] revised - compatibility with new df-prds
18-Aug-24 prdsmulr [same] revised - compatibility with new df-prds
18-Aug-24 prdsplusg [same] revised - compatibility with new df-prds
18-Aug-24 prdsbas [same] revised - compatibility with new df-prds
18-Aug-24 prdssca [same] revised - compatibility with new df-prds
18-Aug-24 prdsval [same] revised - compatibility with new df-prds
18-Aug-24 reldmprds [same] revised - compatibility with new df-prds
18-Aug-24 df-prds [same] revised - fixed the comp part
18-Aug-24 difexd [same] moved from SN's mathbox to main set.mm
18-Aug-24 ifexd [same] moved from SN's mathbox to main set.mm
13-Aug-24 syl6rbb bitr2di compare to bitr2i or bitr2d
12-Aug-24 disjdifr [same] moved from TA's mathbox to main set.mm
7-Aug-24 tdeglem4 [same] revised - eliminated unnecessary antecedent
7-Aug-24 tdeglem3 [same] revised - eliminated unnecessary antecedent
7-Aug-24 tdeglem1 [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbagev2 [same] revised - eliminated unnecessary hypothesis
7-Aug-24 psrbagev1 [same] revised - eliminated unnecessary hypothesis
7-Aug-24 psrbagfsupp [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbagaddcl [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrass1lem [same] revised - eliminated unnecessary hypothesis
7-Aug-24 gsumbagdiag [same] revised - eliminated unnecessary hypothesis
7-Aug-24 gsumbagdiaglem [same] revised - eliminated unnecessary hypothesis
7-Aug-24 psrbagconf1o [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbagconcl [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbaglefi [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbagcon [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbagcl [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbaglesupp [same] revised - eliminated unnecessary antecedent
7-Aug-24 psrbag [same] revised - eliminated unnecessary antecedent
4-Aug-24 rnmpt0 rnmpt0f moved from GS's mathbox to main set.mm
4-Aug-24 rnmptn0 [same] moved from GS's mathbox to main set.mm
31-Jul-24 f1oeq1d [same] moved from GS's mathbox to main set.mm
28-Jul-24 syl6bbr bitr4di compare to bitr4i or bitr4d
26-Jul-24 ascl1 [same] moved from AV's mathbox to main set.mm
24-Jul-24 grpmndd [same] moved from SN's mathbox to main set.mm
24-Jul-24 zringsubgval [same] moved from AV's mathbox to main set.mm
21-Jul-24 syl6rbbr bitr4id order of hypotheses is switched
6-Jul-24 syl6eq eqtrdi compare to eqtri or eqtrd
6-Jul-24 syl6reqr eqtr4id order of hypotheses is switched
2-Jul-24 snn0d [same] moved from GS's mathbox to main set.mm
26-Jun-24 rnresss [same] moved from GS's mathbox to main set.mm
26-Jun-24 fndmexd [same] moved from RR's mathbox to main set.mm
26-Jun-24 iunssf [same] moved from GS's mathbox to main set.mm
26-Jun-24 rp-imass resssxp moved from RP's mathbox to main set.mm
26-Jun-24 sscon34b [same] moved from RP's mathbox to main set.mm
26-Jun-24 rcompleq [same] moved from RP's mathbox to main set.mm
26-Jun-24 funresd [same] moved from GS's mathbox to main set.mmisCyclic_of_subgroup_isDomain
26-Jun-24 cmnmndd [same] moved from SN's mathbox to main set.mm
26-Jun-24 syl6req eqtr2di compare to eqtr2i or eqtr2d
16-Jun-24 syl6eqr eqtr4di compare to eqtr4i or eqtr4d
16-Jun-24 fnun2d [same] moved from MKU's mathbox to main set.mm
16-Jun-24 fnun1d [same] moved from MKU's mathbox to main set.mm
16-Jun-24 fnund [same] moved from MKU's mathbox to main set.mm
16-Jun-24 partfun [same] moved from TA's mathbox to main set.mm
16-Jun-24 elrnmptd [same] moved from GS's mathbox to main set.mm
15-Jun-24 resexd [same] moved from GS's mathbox to main set.mm
10-Jun-24 bj-intss intss2 moved from BJ's mathbox to main set.mm
3-Jun-24 nfcriv nfcri dv condition was removed
31-May-24 ringgrpd [same] moved from SN's mathbox to main set.mm
31-May-24 crnggrpd [same] moved from SN's mathbox to main set.mm
31-May-24 crngringd [same] moved from SN's mathbox to main set.mm
25-May-24 suppcofnd --- deleted; its sole usage now uses
suppcoss
23-May-24 syl5bbr bitr3id compare to bitr3i or bitr3d
23-May-24 elfzd [same] moved from GS's mathbox to main set.mm
23-May-24 elfelzd [same] moved from GS's mathbox to main set.mm
22-May-24 2exp5 [same] moved from AV's mathbox to main set.mm
16-May-24 2exp7 [same] moved from AV's mathbox to main set.mm
13-May-24 syl5rbbr bitr3di order of hypotheses is switched
12-May-24 ioosscn [same] moved from GS's mathbox to main set.mm
12-May-24 iccssred [same] moved from GS's mathbox to main set.mm
12-May-24 cncfcompt2 [same] moved from GS's mathbox to main set.mm
12-May-24 idcncf [same] moved from JM's mathbox to main set.mm
12-May-24 sub1cncf [same] moved from JM's mathbox to main set.mm
12-May-24 sub2cncf [same] moved from JM's mathbox to main set.mm
12-May-24 addcncf [same] moved from GS's mathbox to main set.mm
12-May-24 subcncf [same] moved from GS's mathbox to main set.mm
12-May-24 dvmptresicc [same] moved from GS's mathbox to main set.mm
8-May-24 fexd [same] moved from GS's mathbox to main set.mm
29-Apr-24 elunitcn [same] moved from TA's mathbox to main set.mm
29-Apr-24 elunitrn [same] moved from TA's mathbox to main set.mm
29-Apr-24 unitsscn [same] moved from TA's mathbox to main set.mm
29-Apr-24 itgpowd [same] moved from JPP's mathbox to main set.mm
29-Apr-24 ifpdfbi [same] moved from RP's mathbox to main set.mm
26-Apr-24 bddiblnc [same] moved from BL's mathbox to main set.mm
26-Apr-24 cnicciblnc [same] moved from BL's mathbox to main set.mm
21-Apr-24 nnindd [same] moved from TA's mathbox to main set.mm
17-Apr-24 syl6eqel eqeltrdi compare to eqeltri or eqeltrd
13-Apr-24 unitresl olcnd
13-Apr-24 unitresr orcnd
12-Apr-24 mth8 jcn
12-Apr-24 jcn jcnd
10-Apr-24 syl6eqelr eqeltrrdi compare to eqeltrri or eqeltrrd
29-Mar-24 fvmptdf fvmptd2f
28-Mar-24 --- --- section "Monoid of endofunctions"
moved from AV's mathbox to main set.mm
24-Mar-24 anim12da --- deleted (in JM's mathbox),
duplicate of anim12dan
24-Mar-24 elabd spcedv
23-Mar-24 funfvima2d [same] moved from SP's mathbox to main set.mm
17-Mar-24 uniexd [same] moved from GS's mathbox to main set.mm
16-Mar-24 syl6eleq eleqtrdi compare to eleqtri or eleqtrd
10-Mar-24 syl6eleqr eleqtrrdi compare to eleqtrri or eleqtrrd
29-Feb-24 syl6ss sstrdi compare to sstri or sstrd
27-Feb-24 syl6sseq sseqtrdi compare to sseqtri or sseqtrd
13-Feb-24 syl6eqss eqsstrdi compare to eqsstri or eqsstrd
4-Feb-24 syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd
29-Jan-24 ccatw2s1ccatws2 [same] revised - eliminated unnecessary antecedent
28-Jan-24 ccat2s1fst [same] revised - eliminated unnecessary antecedent
28-Jan-24 ccatw2s1ass [same] revised - eliminated unnecessary antecedent
28-Jan-24 ccat2s1fvw [same] revised - eliminated unnecessary antecedent
28-Jan-24 ccat2s1fvwALT [same] revised - eliminated unnecessary antecedent
28-Jan-24 ccatw2s1p1 [same] revised - eliminated unnecessary antecedent
23-Jan-24 nelb [same] moved from TA's mathbox to main set.mm
22-Jan-24 syl6sseqr sseqtrrdi
21-Jan-24 ccats1val1 [same] revised - eliminated unnecessary antecedent
21-Jan-24 ccat2s1p1 [same] revised - eliminated unnecessary antecedent
21-Jan-24 ccat2s1p2 [same] revised - eliminated unnecessary antecedent
20-Jan-24 nfiund nfiundg
20-Jan-24 bnj1441 bnj1441g
20-Jan-24 cbviinv cbviinvg
20-Jan-24 cbviunv cbviunvg
20-Jan-24 cbviin cbviing
20-Jan-24 cbviun cbviung
20-Jan-24 nfiin nfiing
20-Jan-24 nfiun nfiung
20-Jan-24 nfrex nfrexg
20-Jan-24 nfrexd nfrexdg
20-Jan-24 nfaba1 nfaba1g
20-Jan-24 nfab nfabg
20-Jan-24 hblem hblemg
20-Jan-24 nfsab nfsabg
20-Jan-24 hbab hbabg
17-Jan-24 cbvmptv cbvmptvg
17-Jan-24 cbvmpt cbvmptg
17-Jan-24 cbvmptf cbvmptfg
17-Jan-24 cbvopab1 cbvopab1g
17-Jan-24 mteqand [same] moved from SN's mathbox to main set.mm
15-Jan-24 sseqtr4d sseqtrrd
14-Jan-24 sseqtr4i sseqtrri
14-Jan-24 ccat2s1len [same] revised - eliminated unnecessary antecedents
14-Jan-24 wlklenvclwlk [same] revised - eliminated unnecessary antecedent
13-Jan-24 mndlsmidm [same] moved from AV's mathbox to main set.mm
13-Jan-24 smndlsmidm [same] moved from AV's mathbox to main set.mm
13-Jan-24 cycsubm [same] moved from AV's mathbox to main set.mm
13-Jan-24 cycsubmcl [same] moved from AV's mathbox to main set.mm
13-Jan-24 cycsubmel [same] moved from AV's mathbox to main set.mm
13-Jan-24 mulgnn0gsum [same] moved from AV's mathbox to main set.mm
13-Jan-24 mulgnngsum [same] moved from AV's mathbox to main set.mm
13-Jan-24 gsumxp2 [same] moved from AV's mathbox to main set.mm
13-Jan-24 gsumreidx [same] moved from AV's mathbox to main set.mm
13-Jan-24 gsumsgrpccat [same] moved from AV's mathbox to main set.mm
13-Jan-24 gsumsplit1r [same] moved from AV's mathbox to main set.mm
13-Jan-24 mndbn0 [same] moved from AV's mathbox to main set.mm
13-Jan-24 lidrididd [same] moved from AV's mathbox to main set.mm
13-Jan-24 lidrideqd [same] moved from AV's mathbox to main set.mm
5-Jan-24 --- --- sections "Groups" and "Simple groups"
moved from RR's mathbox to main set.mm
5-Jan-24 rr-php2d phpeqd moved from RR's mathbox to main set.mm
5-Jan-24 phphashd [same] moved from RR's mathbox to main set.mm
5-Jan-24 phphash2d phphashrd moved from RR's mathbox to main set.mm
5-Jan-24 hashelne0d [same] moved from RR's mathbox to main set.mm
5-Jan-24 hash1elsn [same] moved from RR's mathbox to main set.mm
5-Jan-24 gcdmuld gcdmultipled moved from RR's mathbox to main set.mm
5-Jan-24 gcddvdsd dvdsgcdidd moved from RR's mathbox to main set.mm
5-Jan-24 neqcomd [same] moved from RR's mathbox to main set.mm
5-Jan-24 rr-rspce rspcime moved from RR's mathbox to main set.mm
5-Jan-24 rr-elrnmptd elrnmptdv moved from RR's mathbox to main set.mm
5-Jan-24 rr-elrnmpt2d elrnmpt2d moved from RR's mathbox to main set.mm
5-Jan-24 enpr2d [same] moved from RR's mathbox to main set.mm
5-Jan-24 cntrcmnd [same] moved from TA's mathbox to main set.mm
5-Jan-24 cntrabl [same] moved from TA's mathbox to main set.mm
5-Jan-24 syl6eqbr eqbrtrdi compare to eqbrtri or eqbrtrd
5-Jan-24 syl6eqbrr eqbrtrrdi compare to eqbrtrri or eqbrtrrd
4-Jan-24 fimaproj [same] moved from TA's mathbox to main set.mm
4-Jan-24 fproj [same] moved from TA's mathbox to main set.mm
4-Jan-24 mptima [same] moved from GS's mathbox to main set.mm
3-Jan-24 unima [same] moved from GS's mathbox to main set.mm
29-Dec-23 uzidd [same] moved from GS's mathbox to main set.mm
28-Dec-23 eqri [same] moved from TA's mathbox to main set.mm
28-Dec-23 domep dmep moved from SF's mathbox to main set.mm
28-Dec-23 compel velcomp moved from AS's mathbox to main set.mm
28-Dec-23 syl6breq breqtrdi compare to breqtri or breqtrd
26-Dec-23 syl6breqr breqtrrdi compare to breqtrri or breqtrrd
25-Dec-23 prth anim12
25-Dec-23 selpw velpw
17-Dec-23 syl5eqel eqeltrid compare to eqeltri or eqeltrd
13-Dec-23 syl5eqelr eqeltrrid compare to eqeltrri or eqeltrrd
13-Dec-23 syl5eleq eleqtrid compare to eleqtri or eleqtrd
11-Dec-23 syl5eleqr eleqtrrid compare to eleqtrri or eleqtrrd
11-Dec-23 syl5eqner eqnetrrid compare to eqnetrri or eqnetrrd
6-Dec-23 hbaevg deleted
6-Dec-23 hbnaevg naev2 similarity to aev2
4-Dec-23 syl5ss sstrid compare to sstri or sstrd
3-Dec-23 syl5eqss eqsstrid compare to eqsstri or eqsstrd
1-Dec-23 syl5eqssr eqsstrrid compare to eqsstrri or eqsstrrd
28-Nov-23 unitresl [same] moved from GM's mathbox to main set.mm
28-Nov-23 unitresr [same] moved from GM's mathbox to main set.mm
28-Nov-23 nel02 [same] moved from PM's mathbox to main set.mm
28-Nov-23 fvco3d [same] moved from SP's mathbox to main set.mm
28-Nov-23 fzossz [same] moved from GS's mathbox to main set.mm
26-Nov-23 syl5sseq sseqtrid compare to sseqtri or sseqtrd
21-Nov-23 syl5sseqr sseqtrrid
21-Nov-23 eqsstr3d eqsstrrd
21-Nov-23 eqsstr3i eqsstrri
18-Nov-23 fun11iun f1iun labeling consistent with fiun
18-Nov-23 inex2ALTV inex2g moved from PM's mathbox to main set.mm
18-Nov-23 bj-rabbid rabbid moved from BJ's mathbox to main set.mm
18-Nov-23 bj-rabbida rabbida moved from BJ's mathbox to main set.mm
18-Nov-23 elmapresaun [same] moved from SO's mathbox to main set.mm
17-Nov-23 syl5eqbr eqbrtrid compare to eqbrtri or eqbrtrd
13-Nov-23 syl5eqbrr eqbrtrrid compare to eqbrtrri or eqbrtrrd
12-Nov-23 syl5breq breqtrid compare to breqtri or breqtrd
11-Nov-23 syl5breqr breqtrrid compare to breqtrri or breqtrrd
5-Nov-23 ascl0 [same] moved from AV's mathbox to main set.mm
5-Nov-23 fcod [same] moved from GS's mathbox to main set.mm
31-Oct-23 spimv1 spimfv labeling consistent with speimfv
28-Oct-23 bj-2ex 2oex moved from BJ's mathbox to main set.mm
23-Oct-23 bj-alequexv alequexv moved from BJ's mathbox to main set.mm
23-Oct-23 axext2 axexte existential form of ax-ext
23-Oct-23 axext3 axextg more general form of ax-ext
23-Oct-23 axext4 axextb biconditional form of ax-ext
22-Oct-23 spimeh spimew existential version of spimw
22-Oct-23 speiv speivw weak form of speiv
22-Oct-23 axsep2 axsepg
20-Oct-23 xnn0lem1lt [same] moved from TA's mathbox to main set.mm
15-Oct-23 fnssresd [same] moved from GS's mathbox to main set.mm
11-Oct-23 2exanali [same] moved from ATS's mathbox to main set.mm
6-Oct-23 vtocl2d [same] moved from TA's mathbox to main set.mm
4-Oct-23 df-cda df-dju use |_| instead of +c
4-Oct-23 cdaval df-dju use |_| instead of +c
4-Oct-23 cdadju --- use |_| instead of +c
4-Oct-23 xpsc --- +c is no longer used or needed
4-Oct-23 xpscg --- +c is no longer used or needed
4-Oct-23 dfxpspr df-xps changes from +c to a pair of ordered pairs
4-Oct-23 df-xps [same] changes from +c to a pair of ordered pairs
4-Oct-23 xpscfn fnpr2o changes from +c to a pair of ordered pairs
4-Oct-23 xpsc0 fvpr0o changes from +c to a pair of ordered pairs
4-Oct-23 xpsc1 fvpr1o changes from +c to a pair of ordered pairs
4-Oct-23 xpsfrnel2cda xpsfrnel2 changes from +c to a pair of ordered pairs
4-Oct-23 xpscfcda xpscf changes from +c to a pair of ordered pairs
4-Oct-23 dprdpr [same] changes from +c to a pair of ordered pairs
4-Oct-23 dmdprdpr [same] changes from +c to a pair of ordered pairs
2-Oct-23 xpsfeqcda xpsfeq changes from +c to a pair of ordered pairs
2-Oct-23 xpscfv fvprif changes from +c to a pair of ordered pairs
2-Oct-23 xpsfvalcda xpsfval changes from +c to a pair of ordered pairs
2-Oct-23 xpsff1ocda xpsff1o changes from +c to a pair of ordered pairs
2-Oct-23 xpsfrncda xpsfrn changes from +c to a pair of ordered pairs
2-Oct-23 xpsff1o2cda xpsff1o2 changes from +c to a pair of ordered pairs
2-Oct-23 xpsvalcda xpsval changes from +c to a pair of ordered pairs
2-Oct-23 xpslem xpsrnbas changes from +c to a pair of ordered pairs
1-Oct-23 xpsxmetlem [same] changes from +c to a pair of ordered pairs
1-Oct-23 xpstopnlem2 [same] changes from +c to a pair of ordered pairs
1-Oct-23 xpstopnlem1 [same] changes from +c to a pair of ordered pairs
29-Sep-23 xpsaddlem [same] changes from +c to a pair of ordered pairs
26-Sep-23 xpscf xpscfcda
26-Sep-23 xpsfrnel2 xpsfrnel2cda
26-Sep-23 xpsfeq xpsfeqcda
26-Sep-23 xpsff1o2 xpsff1o2cda
26-Sep-23 xpsfrn2 --- deleted
26-Sep-23 xpsfrn xpsfrncda
26-Sep-23 xpsff1o xpsff1ocda
26-Sep-23 xpsfval xpsfvalcda
24-Sep-23 nelpr1 [same] moved from GS's mathbox to main set.mm
24-Sep-23 nelpr2 [same] moved from GS's mathbox to main set.mm
24-Sep-23 breldmd [same] moved from GS's mathbox to main set.mm
24-Sep-23 fvelimad [same] moved from GS's mathbox to main set.mm
24-Sep-23 0un [same] moved from GS's mathbox to main set.mm
24-Sep-23 ovmpt2x2 ovmpox2
24-Sep-23 ovmpt2rdx ovmpordx
24-Sep-23 ovmpt2rdxf ovmpordxf
24-Sep-23 mpt2exxg2 mpoexxg2
24-Sep-23 dmmpt2ssx2 dmmpossx2
24-Sep-23 cbvmpt2x2 cbvmpox2
24-Sep-23 mpt2mptx2 mpomptx2
24-Sep-23 opmpt2ismgm opmpoismgm
24-Sep-23 elrnmpt2id elrnmpoid
24-Sep-23 cbvmpt21 cbvmpo1
24-Sep-23 cbvmpt22 cbvmpo2
23-Sep-23 mpt2bi123f mpobi123f
23-Sep-23 wl-naev naev moved from WL's mathbox to main set.mm
22-Sep-23 bj-spimevw spimevw moved from BJ's mathbox to main set.mm
21-Sep-23 icorempt2 icorempo
21-Sep-23 csbmpt22g csbmpo123
21-Sep-23 xpsval xpsvalcda
20-Sep-23 bj-sels sels moved from BJ's mathbox to main set.mm
20-Sep-23 bj-mpt2mptALT bj-mpomptALT
20-Sep-23 bj-dfmpt2a bj-dfmpoa
20-Sep-23 matmpt2 matmpo
18-Sep-23 mpt2cti mpocti
18-Sep-23 mpt2mptxf mpomptxf
18-Sep-23 rnmpt2ss rnmposs
18-Sep-23 clwwlknonmpt2 clwwlknonmpo
18-Sep-23 cnmpt2pc cnmpopc
17-Sep-23 cdaun endjudisj Changes from +c notation to |_|
17-Sep-23 cdaen djuen Changes from +c notation to |_|
17-Sep-23 cdafn --- |_| is not a function
17-Sep-23 cdaenun djuenun Changes from +c notation to |_|
17-Sep-23 cdadom1 djudom1 Changes from +c notation to |_|
17-Sep-23 cdacomen djucomen Changes from +c notation to |_|
17-Sep-23 cdadom2 djudom2 Changes from +c notation to |_|
17-Sep-23 pwxpndom2cda pwxpndom2 Changes from +c notation to |_|
17-Sep-23 xp2cda xp2dju Changes from +c notation to |_|
17-Sep-23 uncdadom undjudom Changes from +c notation to |_|
17-Sep-23 mapcdaen mapdjuen Changes from +c notation to |_|
17-Sep-23 cdadom3 djudoml Changes from +c notation to |_|
17-Sep-23 pwcdaen pwdjuen Changes from +c notation to |_|
17-Sep-23 infcda1 infdju1 Changes from +c notation to |_|
17-Sep-23 cdaxpdom djuxpdom Changes from +c notation to |_|
17-Sep-23 cdafi djufi Changes from +c notation to |_|
17-Sep-23 cda1dif dju1dif Changes from +c notation to |_|
17-Sep-23 pwcdandom pwdjundom Changes from +c notation to |_|
17-Sep-23 pwcda1 pwdju1 Changes from +c notation to |_|
16-Sep-23 gchcda1 gchdju1 Changes from +c notation to |_|
16-Sep-23 pwcdadom pwdjudom Changes from +c notation to |_|
16-Sep-23 gchcdaidm gchdjuidm Changes from +c notation to |_|
16-Sep-23 cda0en dju0en Changes from +c notation to |_|
16-Sep-23 cdalepw djulepw Changes from +c notation to |_|
16-Sep-23 pwcdaidm pwdjuidm Changes from +c notation to |_|
15-Sep-23 pwxpndom2 pwxpndom2cda
15-Sep-23 isfin4-3 isfin4p1 Changes from +c notation to |_|
15-Sep-23 finngch [same] Changes from +c notation to |_|
15-Sep-23 canthp1 [same] Changes from +c notation to |_|
15-Sep-23 canthp1lem1 [same] Changes from +c notation to |_|
15-Sep-23 canthp1lem2 [same] Changes from +c notation to |_|
15-Sep-23 fnexd [same] moved from GS's mathbox to main set.mm
14-Sep-23 gchdomtri [same] Changes from +c notation to |_|
14-Sep-23 infcdaabs infdjuabs Changes from +c notation to |_|
14-Sep-23 infcda infdju Changes from +c notation to |_|
14-Sep-23 alephadd [same] Changes from +c notation to |_|
13-Sep-23 onacda onadju Changes from +c notation to |_|
13-Sep-23 nnacda nnadju Changes from +c notation to |_|
10-Sep-23 mpt2matmul mpomatmul
10-Sep-23 mpt2frlmd mpofrlmd
10-Sep-23 elovmpt2wrd elovmpowrd
10-Sep-23 fvmpt2curryd fvmpocurryd
10-Sep-23 mpt2curryvald mpocurryvald
10-Sep-23 mpt2curryd mpocurryd
10-Sep-23 tposmpt2 tposmpo
9-Sep-23 cdainf djuinf Changes from +c notation to |_|
8-Sep-23 cda1en dju1en Changes from +c notation to |_|
8-Sep-23 cardacda cardadju Changes from +c notation to |_|
8-Sep-23 cdanum djunum Changes from +c notation to |_|
7-Sep-23 sprmpt2d sprmpod
7-Sep-23 brovmpt2ex brovmpoex
7-Sep-23 mpt2xopoveqd mpoxopoveqd
7-Sep-23 mpt2xopovel mpoxopovel
7-Sep-23 mpt2xopoveq mpoxopoveq
6-Sep-23 bj-speiv speiv moved from BJ's mathbox to main set.mm
5-Sep-23 bj-spimev spimefv moved from BJ's mathbox to main set.mm
5-Sep-23 bj-spimedv spimedv moved from BJ's mathbox to main set.mm
4-Sep-23 mpt2xopynvov0 mpoxopynvov0
4-Sep-23 mpt2xopxprcov0 mpoxopxprcov0
4-Sep-23 mpt2xopx0ov0 mpoxopx0ov0
4-Sep-23 mpt2xopxnop0 mpoxopxnop0
4-Sep-23 mpt2xopynvov0g mpoxopynvov0g
4-Sep-23 mpt2xopn0yelv mpoxopn0yelv
4-Sep-23 mpt2xneldm mpoxneldm
4-Sep-23 mpt2xeldm mpoxeldm
3-Sep-23 jcn [same] moved from GS's mathbox to main set.mm
3-Sep-23 mpt2sn mposn
3-Sep-23 dfmpt2 dfmpo
3-Sep-23 fmpt2co fmpoco
3-Sep-23 relmpt2opab relmpoopab
3-Sep-23 fnmpt2ovd fnmpoovd
3-Sep-23 el2mpt2cl el2mpocl
3-Sep-23 el2mpt2csbcl el2mpocsbcl
3-Sep-23 mptmpt2opabovd mptmpoopabovd
2-Sep-23 mptmpt2opabbrd mptmpoopabbrd
31-Aug-23 mpt2ex mpoex
31-Aug-23 mpt2exga mpoexga
31-Aug-23 mpt2exg mpoexg
31-Aug-23 mpt2exxg mpoexxg
31-Aug-23 dmmpt2g dmmpog
31-Aug-23 dmmpt2ga dmmpoga
31-Aug-23 xpcdaen xpdjuen Changes from +c notation to |_|
30-Aug-23 ovmpt2elrn ovmpoelrn
30-Aug-23 dmmpt2 dmmpo
30-Aug-23 fnmpt2i fnmpoi
30-Aug-23 fnmpt2 fnmpo
28-Aug-23 pigt3 [same] moved from BL's mathbox to main set.mm
27-Aug-23 fmpt2 fmpo
27-Aug-23 fmpt2x fmpox
27-Aug-23 dmmpt2ssx dmmpossx
27-Aug-23 mpt2mpts mpompts
27-Aug-23 mpt2mptsx mpomptsx
27-Aug-23 2mpt20 2mpo0
27-Aug-23 fnfvima2 --- deleted; duplicate of fnfvimad
27-Aug-23 rabeqd --- deleted; duplicate of rabeqdv
27-Aug-23 iunxsngf2 --- deleted; duplicate of iunxsngf
27-Aug-23 brabg2a --- deleted; duplicate of brab2a
27-Aug-23 abeq12 --- deleted; duplicate of abbi1
26-Aug-23 elovmpt2rab1 elovmporab1
26-Aug-23 elovmpt2rab elovmporab
26-Aug-23 elovmpt2 elovmpo
26-Aug-23 elmpt2cl2 elmpocl2
26-Aug-23 elmpt2cl1 elmpocl1
26-Aug-23 elmpt2cl elmpocl
26-Aug-23 mpt2ndm0 mpondm0
24-Aug-23 cdaassen djuassen Changes from +c notation to |_|
23-Aug-23 ovmpt2 ovmpo
23-Aug-23 ovmpt2g ovmpog
23-Aug-23 ovmpt2dv2 ovmpodv2
23-Aug-23 ovmpt2dv ovmpodv
23-Aug-23 ovmpt2df ovmpodf
23-Aug-23 ovmpt2a ovmpoa
23-Aug-23 ovmpt2ga ovmpoga
23-Aug-23 ovmpt2x ovmpox
22-Aug-23 ovmpt2d ovmpod
22-Aug-23 ovmpt2dx ovmpodx
22-Aug-23 ovmpt2dxf ovmpodxf
22-Aug-23 ovmpt2s ovmpos
22-Aug-23 rexrnmpt2 rexrnmpo
22-Aug-23 ralrnmpt2 ralrnmpo
22-Aug-23 df-srdg [same] moved from SO's mathbox to main set.mm
22-Aug-23 issrdg [same] moved from SO's mathbox to main set.mm
22-Aug-23 sdrgid [same] moved from SO's mathbox to main set.mm
22-Aug-23 sdrgss [same] moved from SO's mathbox to main set.mm
22-Aug-23 issdrg2 [same] moved from SO's mathbox to main set.mm
22-Aug-23 acsfn1p [same] moved from SO's mathbox to main set.mm
22-Aug-23 subrgacs [same] moved from SO's mathbox to main set.mm
22-Aug-23 sdrgacs [same] moved from SO's mathbox to main set.mm
22-Aug-23 cntzsdrg [same] moved from SO's mathbox to main set.mm
22-Aug-23 subdrgint [same] moved from TA's mathbox to main set.mm
22-Aug-23 sdrgint [same] moved from TA's mathbox to main set.mm
22-Aug-23 primefld [same] moved from TA's mathbox to main set.mm
22-Aug-23 cntrss [same] moved from TA's mathbox to main set.mm
22-Aug-23 iinssiun [same] moved from TA's mathbox to main set.mm
22-Aug-23 iindif1 [same] moved from TA's mathbox to main set.mm
22-Aug-23 mvlladdd [same] moved from DAW's mathbox to main set.mm
22-Aug-23 rpexpmord [same] moved from SO's mathbox to main set.mm
22-Aug-23 expmordi [same] moved from SO's mathbox to main set.mm
22-Aug-23 pwm1geoserALT pwm1geoser from AV's mathbox; equivalent theorems
22-Aug-23 pwdif [same] moved from AV's mathbox to main set.mm
21-Aug-23 iunssd [same] moved from GS's mathbox to main set.mm
21-Aug-23 elrnmpt2res elrnmpores
21-Aug-23 elrnmpt2 elrnmpo
21-Aug-23 elrnmpt2g elrnmpog
21-Aug-23 reldmmpt2 reldmmpo
21-Aug-23 pm110.643ALT dju1p1e2ALT Changes from +c notation to |_|
21-Aug-23 pm110.643 dju1p1e2 Changes from +c notation to |_|
20-Aug-23 rnmpt2 rnmpo
20-Aug-23 mpt22eqb mpo2eqb
20-Aug-23 mpt2fun mpofun
18-Aug-23 resmpt2 resmpo
18-Aug-23 fconstmpt2 fconstmpo
18-Aug-23 mpt2snif mposnif
18-Aug-23 mpt2difsnif mpodifsnif
17-Aug-23 mpt2mpt mpompt
17-Aug-23 mpt2mptx mpomptx
17-Aug-23 mpt2v mpov
17-Aug-23 cbvmpt2v cbvmpov
17-Aug-23 cbvmpt2 cbvmpo
17-Aug-23 cbvmpt2x cbvmpox
17-Aug-23 mpt20 mpo0
15-Aug-23 nfmpt2 nfmpo
15-Aug-23 nfmpt22 nfmpo2
15-Aug-23 nfmpt21 nfmpo1
14-Aug-23 mpt2eq3dv mpoeq3dv
14-Aug-23 mpt2eq3ia mpoeq3ia
13-Aug-23 mpt2eq3dva mpoeq3dva
12-Aug-23 mpt2eq123i mpoeq123i
12-Aug-23 mpt2eq123dv mpoeq123dv
12-Aug-23 mpt2eq123dva mpoeq123dva
11-Aug-23 mpt2eq12 mpoeq12
11-Aug-23 mpt2eq123 mpoeq123
10-Aug-23 cmpt2 cmpo
6-Aug-23 df-mpt2 df-mpo
31-Jul-23 sbcgfi [same] moved from GM's mathbox to main set.mm
31-Jul-23 csbgfi [same] moved from GM's mathbox to main set.mm
31-Jul-23 sbceqi [same] moved from GM's mathbox to main set.mm
29-Jul-23 19.8ad [same] moved from DAW's mathbox to main set.mm
29-Jul-23 pnfnre2 [same] moved from GS's mathbox to main set.mm
29-Jul-23 spc2d [same] moved from TA's mathbox to main set.mm
29-Jul-23 spc2ed [same] moved from TA's mathbox to main set.mm
25-Jul-23 mpnanrd [same] moved from ML's mathbox to main set.mm
25-Jul-23 f1opr [same] moved from JM's mathbox to main set.mm
25-Jul-23 gsumpr [same] moved from AV's mathbox to main set.mm
25-Jul-23 xpprsng [same] moved from AV's mathbox to main set.mm
25-Jul-23 fnmptd [same] moved from GS's mathbox to main set.mm
22-Jul-23 0neqopab 0nelopab
16-Jul-23 qseq2i [same] moved from PM's mathbox to main set.mm
16-Jul-23 qseq2d [same] moved from PM's mathbox to main set.mm
14-Jul-23 bj-ssb0 sbv moved from BJ's mathbox to main set.mm
8-Jul-23 bj-ssbn sbn from BJ's mathbox; equivalent theorems
8-Jul-23 bj-dfssb2 dfsb7 from BJ's mathbox; equivalent theorems
8-Jul-23 bj-ssbequ2 sbequ2 from BJ's mathbox; equivalent theorems
8-Jul-23 bj-ssbequ1 sbequ1 from BJ's mathbox; equivalent theorems
8-Jul-23 bj-ssbcom3lem sbcom3vv from BJ's mathbox; equivalent theorems
8-Jul-23 bj-ssbssblem sbco2vv from BJ's mathbox; equivalent theorems
7-Jul-23 bj-ssbequ sbequ from BJ's mathbox; equivalent theorems
7-Jul-23 bj-spex spsbe from BJ's mathbox; equivalent theorems
6-Jul-23 bj-rababwv bj-rababw
6-Jul-23 bj-alsb stdpc4 from BJ's mathbox; equivalent theorems
6-Jul-23 bj-ssbim spsbim from BJ's mathbox; equivalent theorems
6-Jul-23 bj-ssbbi spsbbi from BJ's mathbox; equivalent theorems
6-Jul-23 bj-ssbimi sbimi from BJ's mathbox; equivalent theorems
6-Jul-23 bj-ssbbii sbbii from BJ's mathbox; equivalent theorems
6-Jul-23 sn-vexwv sn-vexw
6-Jul-23 bj-sbtv sbtv from BJ's mathbox; equivalent theorems
4-Jul-23 df-ssb df-sb definition change
4-Jul-23 wssb wsb definition change
4-Jul-23 df-sb dfsb1 definition change
4-Jul-23 bj-ssbjust sbjust moved from BJ's mathbox to main set.mm
4-Jul-23 bj-ssbjustlem sbjustlem moved from BJ's mathbox to main set.mm
4-Jul-23 rspcdf [same] moved from EW's mathbox to main set.mm
1-Jul-23 bj-nalset nalset from BJ's mathbox; equivalent theorems
1-Jul-23 bj-spvv spvv moved from BJ's mathbox to main set.mm
25-Jun-23 2reu4 [same] moved from AV's mathbox to main set.mm
25-Jun-23 2reu4a [same] moved from AV's mathbox to main set.mm
25-Jun-23 2reu2 [same] moved from AV's mathbox to main set.mm
25-Jun-23 2reu1 [same] moved from AV's mathbox to main set.mm
25-Jun-23 2rexreu [same] moved from AV's mathbox to main set.mm
25-Jun-23 2rmoswap [same] moved from AV's mathbox to main set.mm
25-Jun-23 2reurmo [same] moved from AV's mathbox to main set.mm
25-Jun-23 2reurex [same] moved from AV's mathbox to main set.mm
25-Jun-23 reuan [same] moved from AV's mathbox to main set.mm
25-Jun-23 rmoanim [same] moved from AV's mathbox to main set.mm
25-Jun-23 reuimrmo [same] moved from AV's mathbox to main set.mm
25-Jun-23 2reu5a [same] moved from AV's mathbox to main set.mm
25-Jun-23 raaan2 [same] moved from AV's mathbox to main set.mm
25-Jun-23 csbconstgi [same] moved from GM's mathbox to main set.mm
18-Jun-23 ssrmo ssrmof moved from TA's mathbox to main set.mm
18-Jun-23 rmoimi [same] moved from AV's mathbox to main set.mm
18-Jun-23 2reu2rex [same] moved from AV's mathbox to main set.mm
14-Jun-23 rru [same] moved from SN's mathbox to main set.mm
10-Jun-23 sbtv [same] moved fron SN's mathbox to main set.mm
8-Jun-23 rnmptc [same] moved from GS's mathbox to main set.mm
8-Jun-23 eqneltri [same] moved from GS's mathbox to main set.mm
6-Jun-23 eceq2i [same] moved from PM's mathbox to main set.mm
6-Jun-23 eceq2d [same] moved from PM's mathbox to main set.mm
6-Jun-23 2sqmo [same] moved from TA's mathbox to main set.mm
6-Jun-23 2sqmod [same] moved from TA's mathbox to main set.mm
6-Jun-23 2sqn0 [same] moved from TA's mathbox to main set.mm
6-Jun-23 bhmafibid2 [same] moved from TA's mathbox to main set.mm
6-Jun-23 bhmafibid1 [same] moved from TA's mathbox to main set.mm
6-Jun-23 nn0sqeq1 [same] moved from TA's mathbox to main set.mm
6-Jun-23 znsqcld [same] moved from TA's mathbox to main set.mm
6-Jun-23 subeqxfrd [same] moved from TA's mathbox to main set.mm
1-Jun-23 eldifsnneq [same] moved from BJ's mathbox to main set.mm
22-May-23 frlmlvec [same] moved from SN's mathbox to main set.mm
20-May-23 dfss7 [same] moved from AV's mathbox to main set.mm
18-May-23 fndmd [same] moved from GS's mathbox to main set.mm
18-May-23 elpreimad [same] moved from GS's mathbox to main set.mm
18-May-23 fnfvimad [same] moved from GS's mathbox to main set.mm
16-May-23 subdivcomb1 [same] moved from SF's mathbox to main set.mm
9-May-23 eel0001 mpsyl4anc moved from AS's mathbox to main set.mm
9-May-23 fprb [same] moved from SF's mathbox to main set.mm
9-May-23 el2v [same] moved from PM's mathbox to main set.mm
30-Apr-23 qseq12 [same] moved from PM's mathbox to main set.mm
27-Apr-23 dedt [same] commuted consequent
27-Apr-23 elimh [same] commuted consequent
16-Apr-23 xrhaus [same] moved from TA's mathbox to main set.mm
7-Apr-23 rexsngf [same] moved from GS's mathbox to main set.mm
2-Apr-23 reuxfr4d [same] moved from TA's mathbox to main set.mm
2-Apr-23 reuxfr3d [same] moved from TA's mathbox to main set.mm
2-Apr-23 2reuswap2 [same] moved from TA's mathbox to main set.mm
2-Apr-23 pm5.31r [same] moved from RM's mathbox to main set.mm
19-Mar-23 soasym [same] moved from SF's mathbox to main set.mm
19-Mar-23 fvmptd2 [same] moved from GS's mathbox to main set.mm
15-Mar-23 mapfvd [same] moved from AV's mathbox to main set.mm
2-Mar-23 wl-hbnaev hbnaev moved from WL's mathbox to main set.mm
21-Feb-23 moimd moimdv align with mobidv, eubidv
16-Feb-23 bj-ldiv ldiv moved from BJ's mathbox to main set.mm
16-Feb-23 bj-rdiv rdiv moved from BJ's mathbox to main set.mm
16-Feb-23 bj-mdiv mdiv moved from BJ's mathbox to main set.mm
16-Feb-23 bj-lineq lineq moved from BJ's mathbox to main set.mm
16-Feb-23 subdivcomb2 [same] moved from SF's mathbox to main set.mm
16-Feb-23 negelrpd [same] moved from GS's mathbox to main set.mm
16-Feb-23 1xr [same] moved from GS's mathbox to main set.mm
16-Feb-23 rexlimdva2 [same] moved from GS's mathbox to main set.mm
16-Feb-23 mvrladdd [same] moved from DAW's mathbox to main set.mm
12-Feb-23 df-tau moved from JK's mathbox to main set.mm
10-Feb-23 rrxmetfi [same] moved from GS's mathbox to main set.mm
10-Feb-23 rrxdsfi [same] moved from GS's mathbox to main set.mm
10-Feb-23 rrxbasefi [same] moved from GS's mathbox to main set.mm
10-Feb-23 addgtge0d [same] moved from AI's mathbox to main set.mm
10-Feb-23 addeq0 [same] moved from TA's mathbox to main set.mm
10-Feb-23 assraddsubd [same] moved from DAW's mathbox to main set.mm
10-Feb-23 xpexd [same] moved from GS's mathbox to main set.mm
10-Feb-23 fvmptd3 [same] moved from GS's mathbox to main set.mm
10-Feb-23 eqeqan1d [same] moved from PM's mathbox to main set.mm
5-Feb-23 srngfn srngstr
30-Jan-23 elsb4lem elsb4v
30-Jan-23 elsb3lem elsb3v
30-Jan-23 equsb3lem equsb3v equsb3lem was a duplicate of equsb3v
19-Jan-23 bj-stdpc4v stdpc4v moved from BJ's mathbox to main set.mm
19-Jan-23 bj-sbftv sbftv moved from BJ's mathbox to main set.mm
19-Jan-23 bj-sbfv sbfv moved from BJ's mathbox to main set.mm
19-Jan-23 bj-equsb1v equsb1v moved from BJ's mathbox to main set.mm
7-Dec-22 decmul1 [same] revised - remove unneeded hypothesis
5-Dec-22 f1oeq2d [same] moved from GS's mathbox to main set.mm
5-Dec-22 dmexd [same] moved from GS's mathbox to main set.mm
13-Oct-22 rmo4f [same] moved from TA's mathbox to main set.mm
13-Oct-22 rmo3f [same] moved from TA's mathbox to main set.mm
13-Oct-22 iunxsngf [same] moved from TA's mathbox to main set.mm
12-Oct-22 df-pfx [same] definition and related theorems
moved from AV's mathbox to main set.mm
9-Oct-22 ndisj [same] moved from RP's mathbox to main set.mm
9-Oct-22 19.9alt 19.3t moved from NM's mathbox to main set.mm
7-Oct-22 exmoeu2 exmoeub biconditional form of exmoeu
7-Oct-22 eubi [same] moved from ATS's mathbox to main set.mm
6-Oct-22 hhsshl csschl hhsshl was in deprecated Part 19
6-Oct-22 hhssbn cssbn hhssbn was in deprecated Part 19
6-Oct-22 ssphl cphssphl ssphl was in deprecated Part 19
6-Oct-22 sspph cphsscph sspph was in deprecated Part 19
4-Oct-22 brresi brresi2
4-Oct-22 opelresi opelidres
4-Oct-22 brres brresi
4-Oct-22 opelres opelresi
4-Oct-22 brresALTV brres moved from PM's mathbox to main set.mm
4-Oct-22 opelresALTV opelres moved from PM's mathbox to main set.mm
4-Oct-22 inxpssres [same] moved from PM's mathbox to main set.mm
4-Oct-22 anbi1cd [same] moved from PM's mathbox to main set.mm
4-Oct-22 anbi1ci [same] moved from PM's mathbox to main set.mm
4-Oct-22 biancomd [same] moved from PM's mathbox to main set.mm
4-Oct-22 biancomi biancom moved from PM's mathbox to main set.mm
4-Oct-22 dvreslem [same] commutation in theorem
3-Oct-22 brrelexi brrelex1i
3-Oct-22 brrelex brrelex1
1-Oct-22 eu5 dfeu this is now a rederivation
1-Oct-22 mo2v dfmo this is now a rederivation
1-Oct-22 mo2 mof "f-version" of df-mo
26-Sep-22 euequ1 euequ
26-Sep-22 eueq1 eueqi inference associated with eueq
18-Sep-22 brinxp2ALTV brinxp2 moved from PM's mathbox to main set.mm
17-Sep-22 zfnuleu --- deleted; use nulmo instead
17-Sep-22 bm2.5ii uniordint more informative label
17-Sep-22 bm1.1 --- deleted; use axextmo instead
14-Sep-22 idinxpres [same] moved from PM's mathbox to main set.mm
14-Sep-22 relinxp [same] moved from PM's mathbox to main set.mm
14-Sep-22 opelinxp [same] moved from PM's mathbox to main set.mm
14-Sep-22 ralanid [same] moved from PM's mathbox to main set.mm
13-Sep-22 epelc epeli inference associated with epelg
13-Sep-22 a1tru trud deduction form of tru
13-Sep-22 trud mptru modus ponens when minor is tru
8-Sep-22 el2v2 elvd moved from PM's mathbox to main set.mm
8-Sep-22 exlimimdd [same] moved from ML's mathbox to main set.mm
4-Sep-22 funresfunco [same] moved from AV's mathbox to main set.mm
3-Sep-22 pwexd [same] moved from GS's mathbox to main set.mm
3-Sep-22 moimd [same] moved from TA's mathbox to main set.mm
3-Sep-22 csbvargi [same] moved from GM's mathbox to main set.mm
1-Sep-22 keepel ifcli inference associated with ifcl
26-Aug-22 elv [same] moved from PM's mathbox to main set.mm
18-Aug-22 eel1111 syl1111anc moved from AS's mathbox to main set.mm
26-Jul-22 wl-jarri jarri moved from WL's mathbox to main set.mm
26-Jul-22 wl-jarli jarli moved from WL's mathbox to main set.mm
25-Jul-22 bj-sb3b sb3b moved from BJ's mathbox to main set.mm
20-Jul-22 brfi1indlem hashdifsnp1
17-Jul-22 mapsnend [same] moved from GS's mathbox to main set.mm
17-Jul-22 mapsnd [same] moved from GS's mathbox to main set.mm
16-Jul-22 bj-cbv3v2 cbv3v2 moved from mathbox to main
12-Jul-22 equviniva equvinva correct a typo
11-Jul-22 prodge02 --- deleted; use prodge0ld instead
11-Jul-22 prodge0i --- deleted; use prodge0rd instead
11-Jul-22 prodge0 --- deleted; use prodge0rd instead
8-Jul-22 spimvALT spimv shorter, and based on the same set of axioms
6-Jul-22 nfimt bj-nfimt moved to mathbox on request of its owner
6-Jul-22 nfimt2 nfimt nfimt was more difficult to prove and has no
application
5-Jul-22 zrhcopsgndif copsgndif
5-Jul-22 ssrind [same] moved from GS's mathbox to main set.mm
3-Jul-22 zrhcofipsgn cofipsgn
1-Jul-22 bj-1ex 1oex moved from BJ's mathbox to main set.mm
23-Jun-22 rspcda --- deleted; use rspcdva instead
17-May-22 ad5ant1345 adantl3r eliminate duplicated theorem
17-May-22 adantlllr adantl3r eliminate duplicated theorem
21-Apr-22 fz1ssfz0 [same] moved from GS's mathbox to main set.mm
21-Apr-22 rabrab [same] moved from TA's mathbox to main set.mm
8-Mar-22 rabbii [same] moved from PM's mathbox to main set.mm
21-Feb-22 cnvoprab [same] moved from TA's mathbox to main set.mm
16-Feb-22 opidg [same] moved from AV's/PM's mathboxes to main set.mm
5-Feb-22 3orel1 [same] moved from SF's mathbox to main set.mm
5-Feb-22 cofmpt [same] moved from TA's mathbox to main set.mm
27-Jan-22 ccatw2s1cl [same] moved from AV's mathbox to main set.mm
27-Jan-22 fzosplitpr [same] moved from AV's mathbox to main set.mm
23-Jan-22 jca2 [same] moved from RM's mathbox to main set.mm
23-Jan-22 eqvincg [same] moved from TA's mathbox to main set.mm
23-Jan-22 idssxp [same] moved from TA's mathbox to main set.mm
23-Jan-22 dfres3 [same] moved from SF's mathbox to main set.mm
23-Jan-22 brv [same] moved from SF's mathbox to main set.mm
23-Jan-22 dfss6 [same] moved from RP's mathbox to main set.mm
23-Jan-22 2r19.29 [same] moved from RM's mathbox to main set.mm
23-Jan-22 n0el [same] moved from RM's mathbox to main set.mm
19-Jan-22 clelsb3f [same] moved from TA's mathbox to main set.mm
9-Jan-22 sumeq2ad [same] moved from GS's mathbox to main set.mm
3-Jan-22 rabidim1 [same] moved from GS's mathbox to main set.mm
2-Jan-22 xlemnf [same] moved from TA's mathbox to main set.mm
2-Jan-22 infxrmnf [same] moved from TA's mathbox to main set.mm
26-Dec-21 3imp231 [same] moved from AS's mathbox to main set.mm
21-Dec-21 bj-eleq2w eleq2w moved from BJ's mathbox to main set.mm
20-Dec-21 bj-eleq1w eleq1w moved from BJ's mathbox to main set.mm
20-Dec-21 rabeqi [same] moved from GS's mathbox to main set.mm
20-Dec-21 rabeqif [same] moved from GS's mathbox to main set.mm
20-Dec-21 bnj21 ssrab3 moved from JB's mathbox to main set.mm
20-Dec-21 funfnd [same] moved from GS's mathbox to main set.mm
20-Dec-21 elrabd [same] moved from GS's mathbox to main set.mm
20-Dec-21 rabasiun --- deleted; use iunrab instead
19-Dec-21 ssdifsn [same] moved from EW's mathbox to main set.mm
19-Dec-21 dvrecg [same] moved from GS's mathbox to main set.mm
19-Dec-21 dvmptdiv [same] moved from GS's mathbox to main set.mm
16-Dec-21 logge0b & al. [same] moved from AV's mathbox to main set.mm
3-Dec-21 ovexd [same] moved from GS's mathbox to main set.mm
2-Dec-21 divcncf [Same] moved from GS's mathbox to main set.mm
2-Dec-21 mptex2 [Same] moved from GS's mathbox to main set.mm
1-Dec-21 unicntop [Same] moved from GS's mathbox to main set.mm
1-Dec-21 cnopn [Same] moved from GS's mathbox to main set.mm
1-Dec-21 volioo [Same] moved from GS's mathbox to main set.mm
26-Nov-21 fvexd [same] moved from GS's mathbox to main set.mm
26-Nov-21 xgepnf [same] moved from TA's mathbox to main set.mm
26-Nov-21 elnelall [same] moved from AV's mathbox to main set.mm
26-Nov-21 nn0le2is012 [same] moved from AV's mathbox to main set.mm
16-Nov-21 rabbia2 [same] moved from GS's mathbox to main set.mm
16-Nov-21 elpwd [same] moved from GS's mathbox to main set.mm
16-Nov-21 elpwi2 [same] moved from GS's mathbox to main set.mm
16-Nov-21 uhgrstrrepelem setsn0fun split into two theorems
16-Nov-21 uhgrstrrepelem basprssdmsets split into two theorems
14-Nov-21 plusgndxnmulrndx [same] moved from AV's mathbox to main set.mm
14-Nov-21 basendxnmulrndx [same] moved from AV's mathbox to main set.mm
12-Nov-21 --- --- math token "Con" changed to "Conn"
12-Nov-21 --- --- math token "PCon" changed to "PConn"
12-Nov-21 --- --- math token "SCon" changed to "SConn"
12-Nov-21 ccon cconn in labels, "connected" is abbreviated by "conn"
12-Nov-21 df-con df-conn
12-Nov-21 cpcon cpconn
12-Nov-21 df-pcon df-pconn
12-Nov-21 cscon csconn
12-Nov-21 df-scon df-sconn
12-Nov-21 iscon isconn
12-Nov-21 iscon2 isconn2
12-Nov-21 conclo connclo
12-Nov-21 contop conntop
12-Nov-21 indiscon indisconn
12-Nov-21 dfcon2 dfconn2
12-Nov-21 consuba connsuba
12-Nov-21 consub connsub
12-Nov-21 cncon cnconn
12-Nov-21 nconsubb nconnsubb
12-Nov-21 consubclo connsubclo
12-Nov-21 conima connima
12-Nov-21 concn conncn
12-Nov-21 iunconlem iunconnlem
12-Nov-21 iuncon iunconn
12-Nov-21 uncon unconn
12-Nov-21 clscon clsconn
12-Nov-21 concompid conncompid
12-Nov-21 concompcon conncompconn
12-Nov-21 concompss conncompss
12-Nov-21 concompcld conncompcld
12-Nov-21 concompclo conncompclo
12-Nov-21 t1conperf t1connperf
12-Nov-21 txcon txconn
12-Nov-21 qtopcon qtopconn
12-Nov-21 conhmph connhmph
12-Nov-21 filcon filconn
12-Nov-21 tgpconcompeqg tgpconncompeqg
12-Nov-21 tgpconcomp tgpconncomp