`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 φ ψ φx φy antecedent)
#
# We can test whether one set is an element of another, and define an abbreviation for the negated version.
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 ==
# We assert the existence of the empty set, a set with no elements.
term (object (∅))
stmt (EmptySet () () (¬ (∈ A (∅))))
#
# == Singleton ==
# 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)))
#
# A set is an element of its singleton: `A ∈ {A}`

.[http://us.metamath.org/mpeuni/snid.html snid], metamath's set.mm, accessed August 5, 2010
stmt (SingletonMembership () () (∈ A (singleton A)))
#
# == Unordered pair ==
# 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))))
#
# An unordered pair contains each of its members: `A ∈ {A, B}`

.
stmt (UnorderedPairLeftMembership () () (∈ A (unorderedPair A B)))
stmt (UnorderedPairRightMembership () () (∈ B (unorderedPair A B)))
#
# Unordered pairs are unordered: `{A, B} = {B, A}`

.
stmt (UnorderedPairCommutativity () () (= (unorderedPair A B) (unorderedPair B A)))
#
# Unordered pair equality can imply equality of members: `{A, C} = {B, C} → A = B`

,[http://us.metamath.org/mpeuni/preqr1.html preqr1], metamath's set.mm, accessed August 4, 2010 and likewise if the unordered pairs are commuted.
#
stmt (UnorderedPairFirstMembersEqual () () (→ (= (unorderedPair A C) (unorderedPair B C)) (= A B)))
stmt (UnorderedPairSecondMembersEqual () () (→ (= (unorderedPair C A) (unorderedPair C B)) (= A B)))
#
# A singleton is equal to an unordered pair with the same element listed twice.
stmt (SingletonUnorderedPair () () (= (singleton A) (unorderedPair A A)))
#
# == Subset ==
# The subset relationship is equivalent to various statements involving membership, unions, intersections, and set differences.[http://us.metamath.org/mpeuni/df-ss.html df-ss]
term (formula (⊆ A B))
stmt (Subset ((A x) (B x)) ()
(↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B)))))
stmt (SubsetMembership () () (→ (⊆ A B) (→ (∈ C A) (∈ C B))))
stmt (SingletonSubset () () (↔ (∈ A B) (⊆ (singleton A) B)))
stmt (UnorderedPairSubset () ()
(↔ (∧ (∈ A C) (∈ B C)) (⊆ (unorderedPair A B) C)))
#
# === 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 ==
# 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 union of two sets is just a special case of the union of a set.
term (object (∪ A B))
stmt (BinaryUnionAsUnion () () (= (∪ A B) (⋃ (unorderedPair A B))))
stmt (BinaryUnion () () (↔ (∈ A (∪ B C)) (∨ (∈ A B) (∈ A C))))
stmt (MembershipUnionRightIntroduction () () (→ (∈ A B) (∈ A (∪ B C))))
stmt (MembershipUnionLeftIntroduction () () (→ (∈ A C) (∈ A (∪ B C))))
stmt (UnionIdempotence () () (= (∪ A A) A))
stmt (UnionSingleton () () (= (⋃ (singleton A)) A))
#
# An unordered pair is the union of singletons for each of its elements.
stmt (UnorderedPairSingleton () ()
(= (unorderedPair A B) (∪ (singleton A) (singleton B))))
#
# === Subsets and unions ===
stmt (SubsetUnion () () (→ (∧ (⊆ A B) (∈ B C)) (⊆ A (⋃ C))))
stmt (MembershipSubsetUnion () () (→ (∈ A B) (⊆ A (⋃ B))))
stmt (SubsetUnionRightIntroduction () ()
(→ (⊆ A B) (⊆ A (∪ B C))))
#
# == Power set ==
# 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 φ))))
stmt (FormulaBound ((A z) (B z)) ((→ φ (∈ z A)))
(↔ (∈ B (separate z A φ)) (subst B z φ)))
#
# The term `{x ∈ A | φ}`

is like a quantifier in the sense that it binds `x`

, and we can change the variable in a similar manner.
stmt (ChangeVariableSeparation
((φx y) (φy x))
((→ (= x y) (↔ φx φy)))
(= (separate x A φx) (separate y A φy)))
#
# == 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))))
stmt (SeparationBuilder () ()
(→ (∧ (= A B) (∀ x (↔ φ ψ))) (= (separate x A φ) (separate x B ψ))))
stmt (buildSeparation () ((↔ φ ψ)) (= (separate x A φ) (separate x A ψ)))
stmt (UnionBuilder () () (→ (= A B) (= (⋃ A) (⋃ B))))
stmt (buildUnion () ((= A B)) (= (⋃ A) (⋃ B)))
stmt (SubsetBuilderLL () () (→ (= B0 B1) (↔ (⊆ A B0) (⊆ A B1))))
stmt (SubsetBuilderRR () () (→ (= A0 A1) (↔ (⊆ A0 B) (⊆ A1 B))))
stmt (buildSubsetLL () ((= B0 B1)) (↔ (⊆ A B0) (⊆ A B1)))
stmt (buildSubsetRR () ((= A0 A1)) (↔ (⊆ A0 B) (⊆ A1 B)))
#
# == 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 ==
#