Logiweb codex of equivalence-relations in pyk

Up Help

ref-1-id-22	var x
ref-0-id-0	equivalence-relations
ref-0-id-1	cdots
ref-0-id-2	object-var
ref-0-id-3	ex-var
ref-0-id-4	ph-var
ref-0-id-5	vaerdi
ref-0-id-6	variabel
ref-0-id-7	op {MissingArg} end op
ref-0-id-8	op2 {MissingArg} comma {MissingArg} end op2
ref-0-id-9	define-equal {MissingArg} comma {MissingArg} end equal
ref-0-id-10	contains-empty {MissingArg} end empty
ref-0-id-11	1deduction {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-12	1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-13	1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-14	1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-15	1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-16	1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-17	1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-18	1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-19	1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-20	1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-21	1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-22	1deduction seven {MissingArg} end 1deduction
ref-0-id-23	1deduction eight {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-24	1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-25	ex1
ref-0-id-26	ex2
ref-0-id-27	ex10
ref-0-id-28	ex20
ref-0-id-29	existential var {MissingArg} end var
ref-0-id-30	{MissingArg} is existential var
ref-0-id-31	exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-32	exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-33	exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-34	exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-35	placeholder-var1
ref-0-id-36	placeholder-var2
ref-0-id-37	placeholder-var3
ref-0-id-38	placeholder-var {MissingArg} end var
ref-0-id-39	{MissingArg} is placeholder-var
ref-0-id-40	ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-41	ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-42	ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-43	ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-44	var big set
ref-0-id-45	object big set
ref-0-id-46	meta big set
ref-0-id-47	zermelo empty set
ref-0-id-48	system zf
ref-0-id-49	1rule mp
ref-0-id-50	1rule gen
ref-0-id-51	1rule repetition
ref-0-id-52	1rule ad absurdum
ref-0-id-53	1rule deduction
ref-0-id-54	1rule exist intro
ref-0-id-55	axiom extensionality
ref-0-id-56	axiom empty set
ref-0-id-57	axiom pair definition
ref-0-id-58	axiom union definition
ref-0-id-59	axiom power definition
ref-0-id-60	axiom separation definition
ref-0-id-61	cheating axiom all disjoint
ref-0-id-62	prop lemma add double neg
ref-0-id-63	prop lemma remove double neg
ref-0-id-64	prop lemma and commutativity
ref-0-id-65	prop lemma auto imply
ref-0-id-66	prop lemma contrapositive
ref-0-id-67	prop lemma first conjunct
ref-0-id-68	prop lemma second conjunct
ref-0-id-69	prop lemma from contradiction
ref-0-id-70	prop lemma from disjuncts
ref-0-id-71	prop lemma iff commutativity
ref-0-id-72	prop lemma iff first
ref-0-id-73	prop lemma iff second
ref-0-id-74	prop lemma imply transitivity
ref-0-id-75	prop lemma join conjuncts
ref-0-id-76	prop lemma mp2
ref-0-id-77	prop lemma mp3
ref-0-id-78	prop lemma mp4
ref-0-id-79	prop lemma mp5
ref-0-id-80	prop lemma mt
ref-0-id-81	prop lemma negative mt
ref-0-id-82	prop lemma technicality
ref-0-id-83	prop lemma weakening
ref-0-id-84	prop lemma weaken or first
ref-0-id-85	prop lemma weaken or second
ref-0-id-86	lemma formula2pair
ref-0-id-87	lemma pair2formula
ref-0-id-88	lemma formula2union
ref-0-id-89	lemma union2formula
ref-0-id-90	lemma formula2separation
ref-0-id-91	lemma separation2formula
ref-0-id-92	lemma subset in power set
ref-0-id-93	lemma power set is subset0
ref-0-id-94	lemma power set is subset
ref-0-id-95	lemma power set is subset0-switch
ref-0-id-96	lemma power set is subset-switch
ref-0-id-97	lemma set equality suff condition
ref-0-id-98	lemma set equality suff condition(t)0
ref-0-id-99	lemma set equality suff condition(t)
ref-0-id-100	lemma set equality skip quantifier
ref-0-id-101	lemma set equality nec condition
ref-0-id-102	lemma reflexivity0
ref-0-id-103	lemma reflexivity
ref-0-id-104	lemma symmetry0
ref-0-id-105	lemma symmetry
ref-0-id-106	lemma transitivity0
ref-0-id-107	lemma transitivity
ref-0-id-108	lemma er is reflexive
ref-0-id-109	lemma er is symmetric
ref-0-id-110	lemma er is transitive
ref-0-id-111	lemma empty set is subset
ref-0-id-112	lemma member not empty0
ref-0-id-113	lemma member not empty
ref-0-id-114	lemma unique empty set0
ref-0-id-115	lemma unique empty set
ref-0-id-116	lemma =reflexivity
ref-0-id-117	lemma =symmetry
ref-0-id-118	lemma =transitivity0
ref-0-id-119	lemma =transitivity
ref-0-id-120	lemma transfer ~is0
ref-0-id-121	lemma transfer ~is
ref-0-id-122	lemma pair subset0
ref-0-id-123	lemma pair subset1
ref-0-id-124	lemma pair subset
ref-0-id-125	lemma same pair
ref-0-id-126	lemma same singleton
ref-0-id-127	lemma union subset
ref-0-id-128	lemma same union
ref-0-id-129	lemma separation subset
ref-0-id-130	lemma same separation
ref-0-id-131	lemma same binary union
ref-0-id-132	lemma intersection subset
ref-0-id-133	lemma same intersection
ref-0-id-134	lemma auto member
ref-0-id-135	lemma eq-system not empty0
ref-0-id-136	lemma eq-system not empty
ref-0-id-137	lemma eq subset0
ref-0-id-138	lemma eq subset
ref-0-id-139	lemma equivalence nec condition0
ref-0-id-140	lemma equivalence nec condition
ref-0-id-141	lemma none-equivalence nec condition0
ref-0-id-142	lemma none-equivalence nec condition1
ref-0-id-143	lemma none-equivalence nec condition
ref-0-id-144	lemma equivalence class is subset
ref-0-id-145	lemma equivalence classes are disjoint
ref-0-id-146	lemma all disjoint
ref-0-id-147	lemma all disjoint-imply
ref-0-id-148	lemma bs subset union(bs/r)
ref-0-id-149	lemma union(bs/r) subset bs
ref-0-id-150	lemma union(bs/r) is bs
ref-0-id-151	theorem eq-system is partition
ref-0-id-152	eq-system of {MissingArg} modulo {MissingArg}
ref-0-id-153	intersection {MissingArg} comma {MissingArg} end intersection
ref-0-id-154	union {MissingArg} end union
ref-0-id-155	binary-union {MissingArg} comma {MissingArg} end union
ref-0-id-156	power {MissingArg} end power
ref-0-id-157	zermelo singleton {MissingArg} end singleton
ref-0-id-158	zermelo pair {MissingArg} comma {MissingArg} end pair
ref-0-id-159	zermelo ordered pair {MissingArg} comma {MissingArg} end pair
ref-0-id-160	{MissingArg} zermelo in {MissingArg}
ref-0-id-161	{MissingArg} is related to {MissingArg} under {MissingArg}
ref-0-id-162	{MissingArg} is reflexive relation in {MissingArg}
ref-0-id-163	{MissingArg} is symmetric relation in {MissingArg}
ref-0-id-164	{MissingArg} is transitive relation in {MissingArg}
ref-0-id-165	{MissingArg} is equivalence relation in {MissingArg}
ref-0-id-166	equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
ref-0-id-167	{MissingArg} is partition of {MissingArg}
ref-0-id-168	{MissingArg} zermelo is {MissingArg}
ref-0-id-169	{MissingArg} is subset of {MissingArg}
ref-0-id-170	not0 {MissingArg}
ref-0-id-171	{MissingArg} zermelo ~in {MissingArg}
ref-0-id-172	{MissingArg} zermelo ~is {MissingArg}
ref-0-id-173	{MissingArg} and0 {MissingArg}
ref-0-id-174	{MissingArg} or0 {MissingArg}
ref-0-id-175	{MissingArg} iff {MissingArg}
ref-0-id-176	the set of ph in {MissingArg} such that {MissingArg} end set