Home | Intuitionistic Logic Explorer Theorem List (p. 18 of 22) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | equsb3lem 1701* | Lemma for equsb3 1702. (Contributed by NM, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | equsb3 1702* | Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.) |
Theorem | sbn 1703 | Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sbim 1704 | Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sbor 1705 | Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sban 1706 | Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sbrim 1707 | Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | sblim 1708 | Substitution with a variable not free in consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) |
Theorem | sb3an 1709 | Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.) |
Theorem | sbbi 1710 | Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) |
Theorem | sblbis 1711 | Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.) |
Theorem | sbrbis 1712 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
Theorem | sbrbif 1713 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
Theorem | sbco2yz 1714* | This is a version of sbco2 1716 where is distinct from . It is a lemma on the way to proving sbco2 1716 which has no distinct variable constraints. (Contributed by Jim Kingdon, 19-Mar-2018.) |
Theorem | sbco2h 1715 | A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.) |
Theorem | sbco2 1716 | A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | sbco2d 1717 | A composition law for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbco2vd 1718* | Version of sbco2d 1717 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbco 1719 | A composition law for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbco3v 1720* | Version of sbco3 1725 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbcocom 1721 | Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.) |
Theorem | sbcomv 1722* | Version of sbcom 1726 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 28-Feb-2018.) |
Theorem | sbcomxyyz 1723* | Version of sbcom 1726 with distinct variable constraints between and , and and . (Contributed by Jim Kingdon, 21-Mar-2018.) |
Theorem | sbco3xzyz 1724* | Version of sbco3 1725 with distinct variable constraints between and , and and . Lemma for proving sbco3 1725. (Contributed by Jim Kingdon, 22-Mar-2018.) |
Theorem | sbco3 1725 | A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.) |
Theorem | sbcom 1726 | A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.) |
Theorem | nfsbt 1727* | Closed form of nfsb 1699. (Contributed by Jim Kingdon, 9-May-2018.) |
Theorem | nfsbd 1728* | Deduction version of nfsb 1699. (Contributed by NM, 15-Feb-2013.) |
Theorem | elsb3 1729* | Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | elsb4 1730* | Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | sb9v 1731* | Like sb9 1732 but with a distinct variable constraint between and . (Contributed by Jim Kingdon, 28-Feb-2018.) |
Theorem | sb9 1732 | Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | sb9i 1733 | Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | hbsbd 1734* | Deduction version of hbsb 1700. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | 2sb5 1735* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | 2sb6 1736* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | sbcom2v 1737* | Lemma for proving sbcom2 1739. It is the same as sbcom2 1739 but with additional distinct variable constraints on and , and on and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbcom2v2 1738* | Lemma for proving sbcom2 1739. It is the same as sbcom2v 1737 but removes the distinct variable constraint on and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbcom2 1739* | Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.) |
Theorem | pm11.07 1740* | Theorem *11.07 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
Theorem | sb6a 1741* | Equivalence for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2sb5rf 1742* | Reversed double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | 2sb6rf 1743* | Reversed double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | dfsb7 1744* | An alternate definition of proper substitution df-sb 1533. By introducing a dummy variable in the definiens, we are able to eliminate any distinct variable restrictions among the variables , , and of the definiendum. No distinct variable conflicts arise because effectively insulates from . To achieve this, we use a chain of two substitutions in the form of sb5 1649, first for then for . Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1745 provides a version where and don't have to be distinct. (Contributed by NM, 28-Jan-2004.) |
Theorem | sb7f 1745* | This version of dfsb7 1744 does not require that and be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1350 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1533 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | sb7af 1746* | An alternative definition of proper substitution df-sb 1533. Similar to dfsb7a 1747 but does not require that and be distinct. Similar to sb7f 1745 in that it involves a dummy variable , but expressed in terms of rather than . (Contributed by Jim Kingdon, 5-Feb-2018.) |
Theorem | dfsb7a 1747* | An alternative definition of proper substitution df-sb 1533. Similar to dfsb7 1744 in that it involves a dummy variable , but expressed in terms of rather than . For a version which only requires rather than and being distinct, see sb7af 1746. (Contributed by Jim Kingdon, 5-Feb-2018.) |
Theorem | sb10f 1748* | Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. (Contributed by NM, 9-May-2005.) |
Theorem | sbid2v 1749* | An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | sbelx 1750* | Elimination of substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbel2x 1751* | Elimination of double substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbalyz 1752* | Move universal quantifier in and out of substitution. Identical to sbal 1753 except that it has an additional distinct variable constraint on and . (Contributed by Jim Kingdon, 29-Dec-2017.) |
Theorem | sbal 1753* | Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.) |
Theorem | sbal1yz 1754* | Lemma for proving sbal1 1755. Same as sbal1 1755 but with an additional distinct variable constraint on and . (Contributed by Jim Kingdon, 23-Feb-2018.) |
Theorem | sbal1 1755* | A theorem used in elimination of disjoint variable restriction on and by replacing it with a distinctor . (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.) |
Theorem | sbexyz 1756* | Move existential quantifier in and out of substitution. Identical to sbex 1757 except that it has an additional distinct variable constraint on and . (Contributed by Jim Kingdon, 29-Dec-2017.) |
Theorem | sbex 1757* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.) |
Theorem | sbalv 1758* | Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.) |
Theorem | exsb 1759* | An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.) |
Theorem | 2exsb 1760* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) |
Theorem | dvelimALT 1761* | Version of dvelim 1768 that doesn't use ax-10 1329. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) |
Theorem | dvelimfv 1762* | Like dvelimf 1766 but with a distinct variable constraint on and . (Contributed by Jim Kingdon, 6-Mar-2018.) |
Theorem | hbsb4 1763 | A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | hbsb4t 1764 | A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1763). (Contributed by NM, 7-Apr-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | nfsb4t 1765 | A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1763). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof rewritten by Jim Kingdon, 9-May-2018.) |
Theorem | dvelimf 1766 | Version of dvelim 1768 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) |
Theorem | dvelimdf 1767 | Deduction form of dvelimf 1766. This version may be useful if we want to avoid ax-17 1350 and use ax-16 1581 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
Theorem | dvelim 1768* |
This theorem can be used to eliminate a distinct variable restriction on
and and replace it with the
"distinctor"
as an antecedent. normally has free and can be read
, and
substitutes for and can be read
. We don't require that and be distinct: if
they aren't, the distinctor will become false (in multiple-element
domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses with , conjoin them, and apply dvelimdf 1767. Other variants of this theorem are dvelimf 1766 (with no distinct variable restrictions) and dvelimALT 1761 (that avoids ax-10 1329). (Contributed by NM, 23-Nov-1994.) |
Theorem | dvelimor 1769* | Disjunctive distinct variable constraint elimination. A user of this theorem starts with a formula (containing ) and a distinct variable constraint between and . The theorem makes it possible to replace the distinct variable constraint with the disjunct ( is just a version of with substituted for ). (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | dveeq1 1770* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.) |
Theorem | dveel1 1771* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
Theorem | dveel2 1772* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
Theorem | sbal2 1773* | Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) |
Theorem | nfsb4or 1774 | A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.) |
Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets." A set can be contained in another set, and this relationship is indicated by the symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects. Here we develop set theory based on the Intuitionistic Zermelo-Fraenkel (IZF) system of [Crosilla] (Crosilla's Constructive Zermelo-Fraenkel (CZF) is not as easy to formalize in metamath because the Axiom of Restricted Separation would require us to develop the ability to classify formulas as bounded formulas, similar to the machinery we have built up for asserting on whether variables are free in formulas). | ||
Axiom | ax-ext 1775* |
Axiom of Extensionality. It states that two sets are identical if they
contain the same elements. Axiom 1 of [Crosilla] (with unnnecessary
quantifiers removed).
Set theory can also be formulated with a single primitive predicate on top of traditional predicate calculus without equality. In that case the Axiom of Extensionality becomes , and equality is defined as . All of the usual axioms of equality then become theorems of set theory. See, for example, Axiom 1 of [TakeutiZaring] p. 8. To use the above "equality-free" version of Extensionality with Metamath's logical axioms, we would rewrite ax-8 1328 through ax-16 1581 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. 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 in ax-ext 1775 can represent any actual variable v1, v2, v3,... . Distinct variable restrictions ($d) prevent us from substituting say v1 for both and . This is in contrast to typical textbook presentations that present actual axioms (except for axioms which involve wff metavariables). In practice, though, the theorems and proofs are essentially the same. The $d restrictions make each of the infinite axioms generated by the ax-ext 1775 scheme exactly logically equivalent to each other and in particular to the actual axiom of the textbook version. (Contributed by NM, 5-Aug-1993.) |
Theorem | axext3 1776* | A generalization of the Axiom of Extensionality in which and need not be distinct. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | axext4 1777* | 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 1775. (Contributed by NM, 14-Nov-2008.) |
Syntax | cab 1778 | Introduce the class builder or class abstraction notation ("the class of sets such that is true"). Our class variables , , etc. range over class builders (sometimes implicitly). Note that a set variable can be expressed as a class builder per theorem cvjust 1787, justifying the assignment of set variables to class variables via the use of cv 1323. |
Definition | df-clab 1779 |
Define class abstraction notation (so-called by Quine), also called a
"class builder" in the literature. and need not be distinct.
Definition 2.1 of [Quine] p. 16. Typically,
will have as a
free variable, and " " is read "the class of all sets
such that is true." We do not define in
isolation but only as part of an expression that extends or
"overloads"
the
relationship.
This is our first use of the symbol to connect classes instead of sets. The syntax definition wcel 1326, which extends or "overloads" the wel 1327 definition connecting set variables, requires that both sides of be a class. In df-cleq 1785 and df-clel 1788, we introduce a new kind of variable (class variable) that can substituted with expressions such as . In the present definition, the on the left-hand side is a set variable. Syntax definition cv 1323 allows us to substitute a set variable for a class variable: all sets are classes by cvjust 1787 (but not necessarily vice-versa). For a full description of how classes are introduced and how to recover the primitive language, see the discussion in Quine (and under abeq2 1897 for a quick overview). 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 called the "axiom of class comprehension" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. He calls the construction a "class term". For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 5-Aug-1993.) |
Theorem | abid 1780 | Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.) |
Theorem | hbab1 1781* | Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfsab1 1782* | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbab 1783* | Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 1-Mar-1995.) |
Theorem | nfsab 1784* | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Definition | df-cleq 1785* |
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 , which is not a theorem of logic but rather presupposes the Axiom of Extensionality (see theorem axext4 1777). We therefore include this axiom as a hypothesis, so that the use of Extensionality is properly indicated. We could avoid this complication by introducing a new symbol, say =_{2}, in place of . This would also have the advantage of making elimination of the definition straightforward, so that we could eliminate Extensionality as a hypothesis. We would then also have the advantage of being able to identify in various proofs exactly where Extensionality truly comes into play rather than just being an artifact of a definition. One of our theorems would then be =_{2} by invoking Extensionality. 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 1779, df-clel 1788, and abeq2 1897. In the form of dfcleq 1786, this is called the "axiom of extensionality" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 15-Sep-1993.) |
Theorem | dfcleq 1786* | The same as df-cleq 1785 with the hypothesis removed using the Axiom of Extensionality ax-ext 1775. (Contributed by NM, 15-Sep-1993.) |
Theorem | cvjust 1787* | 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 1323, which allows us to substitute a set variable for a class variable. See also cab 1778 and df-clab 1779. Note that this is not a rigorous justification, because cv 1323 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." (Contributed by NM, 7-Nov-2006.) |
Definition | df-clel 1788* |
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 1785 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 1785 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with set variables (see cleljust 1689), so we don't include any
set theory axiom as a hypothesis. See also comments about the syntax
under df-clab 1779.
This is called the "axiom of membership" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqriv 1789* | Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqrdv 1790* | Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.) |
Theorem | eqrdav 1791* | Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.) |
Theorem | eqid 1792 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20: "Therefore, inquiring why a thing is itself, it's inquiring nothing; ... saying that the thing is itself constitutes the sole reasoning and the sole cause, in every case, to the question of why the man is man or the musician musician."). (Thanks to Stefan Allan and Benoît Jubin for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by Benoît Jubin, 14-Oct-2017.) |
Theorem | eqidd 1793 | Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.) |
Theorem | eqcom 1794 | Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqcoms 1795 | Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqcomi 1796 | Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqcomd 1797 | Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) |
Theorem | eqeq1 1798 | Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqeq1i 1799 | Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Theorem | eqeq1d 1800 | Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |