`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 a b x y z w)
tvar (object A B C A0 A1 B0 B1)
tvar (formula φ ψ φx φy antecedent)
#
# == Set membership ==
# We can test whether one set is an element of another, and define an abbreviation for the negated version.
term (formula (∈ A 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)))
#
# == Ordered pair ==
# An ordered pair has a first element and a second element, and two ordered pairs are equal if and only if their first elements are equal and their second elements are equal.
term (object (orderedPair A B))
stmt (OrderedPairTheorem () () (↔ (= (orderedPair A0 B0) (orderedPair A1 B1)) (∧ (= A0 A1) (= B0 B1))))
#
# We can extract the first or second element of an ordered pair.
term (object (1st A))
stmt (First () () (= (1st (orderedPair A B)) A))
term (object (2nd A))
stmt (Second () () (= (2nd (orderedPair A B)) B))
#
# == Relations ==
# A relation is a set of ordered pairs. We define `relation A`

as a formula meaning "A is a relation". We customarily use the letters `R, S, and T`

for relations.
term (formula (relation A))
stmt (Relation ((A z)) ()
(↔ (relation A) (∀ z (→ (∈ z A) (∃ x (∃ y (= z (orderedPair x y))))))))
tvar (object R S T)
#
# The Cartesian product of two sets is the set of all ordered pairs consisting of one set from the first given set and one set from the second given set.[http://us.metamath.org/mpeuni/opelxp.html opelxp], metamath's set.mm, accessed November 3, 2010
term (object (× A B))
stmt (MembershipCartesianProduct
((A b a) (B b a) (C b a)) ()
(↔ (∈ C (× A B))
(∃ a (∃ b (∧
(= C (orderedPair a b)) (∧ (∈ a A) (∈ b B)))))))
stmt (OrderedPairCartesianProduct () ()
(↔ (∈ (orderedPair A0 B0) (× A B)) (∧ (∈ A0 A) (∈ B0 B))))
stmt (FirstSecondCartesianProduct () ()
(→ (∈ A (× B C)) (∧ (∈ (1st A) B) (∈ (2nd A) C))))
#
# The domain of a relation is a set consisting of all of the first elements of the ordered pairs in the relation. Our definition, and the theorems that follow, do not require `R`

to be a relation, but they aren't especially interesting if it is not.
term (object (domain A))
stmt (Domain ((B y) (R y)) ()
(↔ (∈ B (domain R)) (∃ y (∈ (orderedPair B y) R))))
stmt (DomainSingletonRelation () ()
(= (domain (singleton (orderedPair A B))) (singleton A)))
#
# The range is a set containing exactly the values which the second members of the ordered pairs in the relation can take on (as opposed to the other common definition, which is a set which is a superset of what we call the range).
term (object (range A))
stmt (Range ((B x) (R x)) ()
(↔ (∈ B (range R)) (∃ x (∈ (orderedPair x B) R))))
stmt (RangeSingletonRelation () ()
(= (range (singleton (orderedPair A B))) (singleton B)))
#
# == 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 Ghilbert 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 (OrderedPairBuilder () () (→ (∧ (= A0 A1) (= B0 B1)) (= (orderedPair A0 B0) (orderedPair A1 B1))))
stmt (OrderedPairBuilderLL () () (→ (= B0 B1) (= (orderedPair A B0) (orderedPair A B1))))
stmt (buildOrderedPairLLInConsequent ()
((→ antecedent (= B0 B1)))
(→ antecedent (= (orderedPair A B0) (orderedPair A B1))))
stmt (OrderedPairBuilderRR () () (→ (= A0 A1) (= (orderedPair A0 B) (orderedPair A1 B))))
stmt (buildOrderedPairRRInConsequent ()
((→ antecedent (= A0 A1)))
(→ antecedent (= (orderedPair A0 B) (orderedPair A1 B))))
stmt (buildSeparation () ((↔ φ ψ)) (= (separate x A φ) (separate x A ψ)))
stmt (UnionBuilder () () (→ (= A B) (= (⋃ A) (⋃ B))))
stmt (buildUnion () ((= A B)) (= (⋃ A) (⋃ B)))
stmt (FirstBuilder () () (→ (= A B) (= (1st A) (1st B))))
stmt (SecondBuilder () () (→ (= A B) (= (2nd A) (2nd B))))
stmt (DomainBuilder () () (→ (= R S) (= (domain R) (domain S))))
stmt (RangeBuilder () () (→ (= R S) (= (range R) (range S))))
#
# == 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 ==
#