`term`

rather than `def`

) and leaves a more comprehensive set of theorems about each of these topics to other places.
#
# == Variables, objects (classes), and membership ==
#
# We build on [[Interface:Classical propositional calculus|propositional logic]] and [[Interface:First-order logic with quantifiability|first-order logic]] (including equality):
#
param (CLASSICAL Classical_propositional_calculus.ghi () "")
param (FIRSTORDER First-order_logic_with_quantifiability.ghi (CLASSICAL) "")
#
# First-order logic provides us with two kinds: `variable`

is a variable, which represents a set and can be quantified over, and `object`

is an expression which represents a set. For example, a variable might be `x`

, `y`

, or `z`

, but an object could be the singleton `{ x }`

, the unordered pair `{ x, y }`

, the ordered pair `〈 x, y 〉`

, etc. To some extent the concepts of variable and object correspond to set and class in some theories (like metamath's set.mm), but one key difference is that we have no [[w:proper class|proper classes]] thanks to the [[Interface:Axiom of quantifiability|axiom of quantifiability]].
#
var (object x y z w)
tvar (object A B C A0 A1 B0 B1)
tvar (formula φ antecedent)
#
# We can test whether one set is an element of another
term (formula (∈ A B))
#
# Here are two ways of combining membership with a substitution:
stmt (MembershipForAll ((A x) (B x)) ()
(↔ (∈ A B) (∀ x (→ (= x A) (∈ x B)))))
stmt (MembershipThereExists ((A x) (B x)) ()
(↔ (∈ A B) (∃ x (∧ (= x A) (∈ x B)))))
#
# == Empty set, singletons, and unordered pairs ==
# We assert the existence of the empty set, a set with no elements.
term (object (∅))
stmt (EmptySet () () (¬ (∈ A (∅))))
#
# Given a set, we can form a set `{ s }`

which has only it as an element.[http://us.metamath.org/mpeuni/elsncg.html elsncg], metamath's set.mm, accessed August 7, 2010
term (object (singleton A))
stmt (Singleton () () (↔ (∈ A (singleton B)) (= A B)))
#
# Given two sets, we can form a unordered pair `{ s, t }`

which has only those sets as elements.
term (object (unorderedPair A B))
stmt (UnorderedPair () () (↔ (∈ B (unorderedPair A0 A1)) (∨ (= B A0) (= B A1))))
#
# == Subset ==
#
# We define the subset relationship.
term (formula (⊆ A B))
stmt (Subset ((A x) (B x)) ()
(↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B)))))
#
# === Partial order ===
# The subset relationship has the three properties of a [[w:Partially ordered set|partial order]]. That is, it is reflexive, antisymmetric, and transitive.
#
stmt (SubsetReflexivity () () (⊆ A A))
stmt (SubsetAntisymmetry () () (→ (∧ (⊆ A B) (⊆ B A)) (= A B)))
stmt (SubsetTransitivity () () (→ (∧ (⊆ A B) (⊆ B C)) (⊆ A C)))
#
# == Union and power set ==
# The union of a set has as its elements everything which is an element of some set in the given set.
term (object (⋃ A))
stmt (Union ((A x) (B x)) () (↔ (∈ B (⋃ A)) (∃ x (∧ (∈ B x) (∈ x A)))))
#
# The power set of a set has as its elements all of the subsets of the given set.
term (object (power A))
stmt (PowerSet () () (↔ (∈ B (power A)) (⊆ B A)))
#
# == Separation ==
# We define `{x ∈ A | φ}`

, the set of all elements in `A`

which also satisfy `φ`

. Although we write `{x ∈ A | φ}`

informally, for JHilbert it needs to be `(separate x A φ)`

.
term (object (separate x A φ) (x A))
stmt (Separation () ()
(↔ (∈ C (separate x A φ)) (∧ (∈ C A) (subst C x φ))))
#
# == Builders ==
# Equals can be substituted for equals, in the context of set operations.
#
stmt (MembershipBuilderLL () () (→ (= B0 B1) (↔ (∈ A B0) (∈ A B1))))
stmt (MembershipBuilderRR () () (→ (= A0 A1) (↔ (∈ A0 B) (∈ A1 B))))
stmt (buildMembershipLL () ((= B0 B1)) (↔ (∈ A B0) (∈ A B1)))
stmt (buildMembershipRR () ((= A0 A1)) (↔ (∈ A0 B) (∈ A1 B)))
stmt (buildMembershipLLInConsequent ()
((→ antecedent (= B0 B1)))
(→ antecedent (↔ (∈ A B0) (∈ A B1))))
stmt (buildMembershipRRInConsequent ()
((→ antecedent (= A0 A1)))
(→ antecedent (↔ (∈ A0 B) (∈ A1 B))))
stmt (SingletonBuilder () () (→ (= A B) (= (singleton A) (singleton B))))
stmt (UnorderedPairBuilder () () (→ (∧ (= A0 B0) (= A1 B1)) (= (unorderedPair A0 A1) (unorderedPair B0 B1))))
#
# == Extensionality ==
# Sets with the same elements are equal.
stmt (Extensionality ((A z) (B z)) () (→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B)))
stmt (applyExtensionality ((A x) (B x)) ((↔ (∈ x A) (∈ x B))) (= A B))
#
# == References ==
#