| Metamath Proof Explorer | < Previous Next > | |
| Browser slow? Try the
Unicode version. |
| Color key: | (1-11257) |
(11258-12844) |
(12845-19026) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | moexex 2101 | "At most one" double quantification. |
| Theorem | moexexv 2102 | "At most one" double quantification. |
| Theorem | 2moex 2103 | Double quantification with "at most one." |
| Theorem | 2euex 2104 | Double quantification with existential uniqueness. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| Theorem | 2eumo 2105 | Double quantification with existential uniqueness and "at most one." |
| Theorem | 2eu2ex 2106 | Double existential uniqueness. |
| Theorem | 2moswap 2107 | A condition allowing swap of "at most one" and existential quantifiers. |
| Theorem | 2euswap 2108 | A condition allowing swap of uniqueness and existential quantifiers. |
| Theorem | 2exeu 2109 | Double existential uniqueness implies double uniqueness quantification. |
| Theorem | 2mo 2110 | Two equivalent expressions for double "at most one." |
| Theorem | 2mos 2111 | Double "exists at most one", using implicit substitition. |
| Theorem | 2eu1 2112 | Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. |
| Theorem | 2eu2 2113 | Double existential uniqueness. |
| Theorem | 2eu3 2114 | Double existential uniqueness. |
| Theorem | 2eu4 2115 |
This theorem provides us with a definition of double existential
uniqueness ("exactly one |
| Theorem | 2eu5 2116 |
An alternate definition of double existential uniqueness (see 2eu4 2115).
A mistake sometimes made in the literature is to use |
| Theorem | 2eu6 2117 | Two equivalent expressions for double existential uniqueness. |
| Theorem | 2eu7 2118 | Two equivalent expressions for double existential uniqueness. |
| Theorem | 2eu8 2119 |
Two equivalent expressions for double existential uniqueness. Curiously,
we can put |
| Theorem | euequ1 2120 | Equality has existential uniqueness. Special case of eueq1 2673 proved using only predicate calculus. (Contributed by Stefan Allan, 4-Dec-2008.) |
| Theorem | exists1 2121 | Two ways to express "only one thing exists." The left-hand side requires only one variable to express this. Both sides are false in set theory; see theorem dtru 3662. |
| Theorem | exists2 2122 | A condition implying that at least two things exist. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| ZF Set Theory - start with the Axiom of Extensionality | ||
| Introduce the Axiom of Extensionality | ||
| Axiom | ax-ext 2123 |
Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It
states that two sets are identical if they contain the same elements.
Axiom Ext of [BellMachover] p.
461.
Set theory can also be formulated with a single primitive
predicate
To use the above "equality-free" version of Extensionality with Metamath's logical axioms, we would rewrite ax-8 1594 through ax-16 1854 with equality expanded according to the above definition. Some of those axioms could be proved from set theory and would be redundant. Not all of them are redundant, since our axioms of predicate calculus make essential use of equality for the proper substitution that is a primitive notion in traditional predicate calculus. A study of such an axiomatization would be an interesting project for someone exploring the foundations of logic.
General remarks: Our set theory axioms are presented using
defined
connectives (
It is important to understand that strictly speaking, all of our set
theory axioms are really schemes that represent an infinite number of
actual axioms. This is inherent in the design of Metamath
("metavariable math"), which manipulates only metavariables.
For
example, the metavariable |
| Theorem | axext2 2124 |
The Axiom of Extensionality (ax-ext 2123) restated so that it postulates
the existence of a set |
| Theorem | axext3 2125 |
A generalization of the Axiom of Extensionality in which |
| Theorem | axext4 2126 | A bidirectional version of Extensionality. Although this theorem "looks" like it is just a definition of equality, it requires the Axiom of Extensionality for its proof under our axiomatization. See the comments for ax-ext 2123 and df-cleq 2134. |
| Theorem | bm1.1 2127 | Any set defined by a property is the only set defined by that property. Theorem 1.1 of [BellMachover] p. 462. |
| Class abstractions (a.k.a. class builders) | ||
| Syntax | cab 2128 |
Introduce the class builder or class abstraction notation ("the class of
sets |
| Definition | df-clab 2129 |
Define class abstraction notation (so-called by Quine), also called a
"class builder" in the literature.
This is our first use of the Because class variables can be substituted with compound expressions and set variables cannot, it is often useful to convert a theorem containing a free set variable to a more general version with a class variable. This is done with theorems such as vtoclg 2588 which is used, for example, to convert elirrv 5933 to elirr 5934. |
| Theorem | abid 2130 | Simplification of class abstraction notation when the free and bound variables are identical. |
| Theorem | hbab1 2131 | Bound-variable hypothesis builder for a class abstraction. |
| Theorem | hbab 2132 | Bound-variable hypothesis builder for a class abstraction. |
| Theorem | hbabd 2133 | Deduction form of bound-variable hypothesis builder hbab 2132. |
| Definition | df-cleq 2134 |
Define the equality connective between classes. Definition 2.7 of
[Quine] p. 18. Also Definition 4.5 of
[TakeutiZaring] p. 13; Chapter 4
provides its justification and methods for eliminating it. Note that
its elimination will not necessarily result in a single wff in the
original language but possibly a "scheme" of wffs.
This is an example of a somewhat "risky" definition, meaning
that it has
a more complex than usual soundness justification (outside of Metamath),
because it "overloads" or reuses the existing equality symbol
rather
than introducing a new symbol. This allows us to make statements that
may not hold for the original symbol. For example, it permits us to
deduce
We could avoid this complication by introducing a new symbol, say
=2,
in place of However, to conform to literature usage, we retain this overloaded definition. This also makes some proofs shorter and probably easier to read, without the constant switching between two kinds of equality. See also comments under df-clab 2129, df-clel 2137, and abeq2 2248. |
| Theorem | dfcleq 2135 | The same as df-cleq 2134 with the hypothesis removed using the Axiom of Extensionality ax-ext 2123. |
| Theorem | cvjust 2136 | Every set is a class. Proposition 4.9 of [TakeutiZaring] p. 13. This theorem shows that a set variable can be expressed as a class abstraction. This provides a motivation for the class syntax construction cv 1585, which allows us to substitute a set variable for a class variable. See also cab 2128 and df-clab 2129. Note that this is not a rigorous justification, because cv 1585 is used as part of the proof of this theorem, but a careful argument can be made outside of the formalism of Metamath, for example as is done in Chapter 4 of Takeuti and Zaring. See also the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class." |
| Definition | df-clel 2137 |
Define the membership connective between classes. Theorem 6.3 of
[Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we
adopt as a definition. See these references for its metalogical
justification. Note that like df-cleq 2134 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2134 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with set variables (see cleljust 1979), so we don't include any
set theory axiom as a hypothesis. See also comments about the syntax
under df-clab 2129. Alternate definitions of |
| Theorem | eqriv 2138 | Infer equality of classes from equivalence of membership. |
| Theorem | eqrdv 2139 | Deduce equality of classes from equivalence of membership. |
| Theorem | eqrdav 2140 | Deduce equality of classes from an equivalence of membership that depends on the membership variable. |
| Theorem | eqid 2141 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). (Thanks to Stefan Allan for this information.) |
| Theorem | eqidd 2142 | Class identity law with antecedent. |
| Theorem | eqcom 2143 | Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. |
| Theorem | eqcoms 2144 | Inference applying commutative law for class equality to an antecedent. |
| Theorem | eqcomi 2145 | Inference from commutative law for class equality. |
| Theorem | eqcomd 2146 | Deduction from commutative law for class equality. |
| Theorem | eqeq1 2147 | Equality implies equivalence of equalities. |
| Theorem | eqeq1i 2148 | Inference from equality to equivalence of equalities. |
| Theorem | eqeq1d 2149 | Deduction from equality to equivalence of equalities. |
| Theorem | eqeq2 2150 | Equality implies equivalence of equalities. |
| Theorem | eqeq2i 2151 | Inference from equality to equivalence of equalities. |
| Theorem | eqeq2d 2152 | Deduction from equality to equivalence of equalities. |
| Theorem | eqeq12 2153 | Equality relationship among 4 classes. |
| Theorem | eqeq12i 2154 | A useful inference for substituting definitions into an equality. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | eqeq12d 2155 | A useful inference for substituting definitions into an equality. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | eqeqan12d 2156 | A useful inference for substituting definitions into an equality. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | eqeqan12rd 2157 | A useful inference for substituting definitions into an equality. |
| Theorem | eqtr 2158 | Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. |
| Theorem | eqtr2 2159 | A transitive law for class equality. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | eqtr3 2160 | A transitive law for class equality. |
| Theorem | eqtri 2161 | An equality transitivity inference. |
| Theorem | eqtr2i 2162 | An equality transitivity inference. |
| Theorem | eqtr3i 2163 | An equality transitivity inference. |
| Theorem | eqtr4i 2164 | An equality transitivity inference. |
| Theorem | 3eqtri 2165 | An inference from three chained equalities. |
| Theorem | 3eqtrri 2166 | An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr2i 2167 | An inference from three chained equalities. |
| Theorem | 3eqtr2ri 2168 | An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr3i 2169 | An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr3ri 2170 | An inference from three chained equalities. |
| Theorem | 3eqtr4i 2171 | An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr4ri 2172 | An inference from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | eqtrd 2173 | An equality transitivity deduction. |
| Theorem | eqtr2d 2174 | An equality transitivity deduction. |
| Theorem | eqtr3d 2175 | An equality transitivity equality deduction. |
| Theorem | eqtr4d 2176 | An equality transitivity equality deduction. |
| Theorem | 3eqtrd 2177 | A deduction from three chained equalities. |
| Theorem | 3eqtrrd 2178 | A deduction from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr2d 2179 | A deduction from three chained equalities. |
| Theorem | 3eqtr2rd 2180 | A deduction from three chained equalities. |
| Theorem | 3eqtr3d 2181 | A deduction from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr3rd 2182 | A deduction from three chained equalities. |
| Theorem | 3eqtr4d 2183 | A deduction from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | 3eqtr4rd 2184 | A deduction from three chained equalities. |
| Theorem | syl5eq 2185 | An equality transitivity deduction. |
| Theorem | syl5eqOLD 2186 | An equality transitivity deduction. |
| Theorem | syl5req 2187 | An equality transitivity deduction. |
| Theorem | syl5reqOLD 2188 | An equality transitivity deduction. |
| Theorem | syl5eqr 2189 | An equality transitivity deduction. |
| Theorem | syl5eqrOLD 2190 | An equality transitivity deduction. |
| Theorem | syl5reqr 2191 | An equality transitivity deduction. |
| Theorem | syl5reqrOLD 2192 | An equality transitivity deduction. |
| Theorem | syl6eq 2193 | An equality transitivity deduction. |
| Theorem | syl6req 2194 | An equality transitivity deduction. |
| Theorem | syl6eqr 2195 | An equality transitivity deduction. |
| Theorem | syl6reqr 2196 | An equality transitivity deduction. |
| Theorem | sylan9eq 2197 | An equality transitivity deduction. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
| Theorem | sylan9req 2198 | An equality transitivity deduction. |
| Theorem | sylan9eqr 2199 | An equality transitivity deduction. |
| Theorem | 3eqtr3g 2200 | A chained equality inference, useful for converting from definitions. |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |