|
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
|
