HomeHome Intuitionistic Logic Explorer
Theorem List (p. 18 of 22)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1701-1800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremequsb3lem 1701* Lemma for equsb3 1702. (Contributed by NM, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremequsb3 1702* Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.)
 
Theoremsbn 1703 Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 
Theoremsbim 1704 Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 
Theoremsbor 1705 Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 
Theoremsban 1706 Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 
Theoremsbrim 1707 Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremsblim 1708 Substitution with a variable not free in consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.)
   =>   
 
Theoremsb3an 1709 Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
 
Theoremsbbi 1710 Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
 
Theoremsblbis 1711 Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
   =>   
 
Theoremsbrbis 1712 Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
   =>   
 
Theoremsbrbif 1713 Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
   &       =>   
 
Theoremsbco2yz 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.)

 F/   =>   
 
Theoremsbco2h 1715 A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
   =>   
 
Theoremsbco2 1716 A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)

 F/   =>   
 
Theoremsbco2d 1717 A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
   &       &       =>   
 
Theoremsbco2vd 1718* Version of sbco2d 1717 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Feb-2018.)
   &       &       =>   
 
Theoremsbco 1719 A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
 
Theoremsbco3v 1720* Version of sbco3 1725 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Feb-2018.)
 
Theoremsbcocom 1721 Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.)
 
Theoremsbcomv 1722* Version of sbcom 1726 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 28-Feb-2018.)
 
Theoremsbcomxyyz 1723* Version of sbcom 1726 with distinct variable constraints between and , and and . (Contributed by Jim Kingdon, 21-Mar-2018.)
 
Theoremsbco3xzyz 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.)
 
Theoremsbco3 1725 A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
 
Theoremsbcom 1726 A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
 
Theoremnfsbt 1727* Closed form of nfsb 1699. (Contributed by Jim Kingdon, 9-May-2018.)
 F/  F/
 
Theoremnfsbd 1728* Deduction version of nfsb 1699. (Contributed by NM, 15-Feb-2013.)

 F/   &     F/   =>     F/
 
Theoremelsb3 1729* Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremelsb4 1730* Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremsb9v 1731* Like sb9 1732 but with a distinct variable constraint between and . (Contributed by Jim Kingdon, 28-Feb-2018.)
 
Theoremsb9 1732 Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
 
Theoremsb9i 1733 Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
 
Theoremhbsbd 1734* Deduction version of hbsb 1700. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
   &       &       =>   
 
Theorem2sb5 1735* Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
 
Theorem2sb6 1736* Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
 
Theoremsbcom2v 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.)
 
Theoremsbcom2v2 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.)
 
Theoremsbcom2 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.)
 
Theorempm11.07 1740* Theorem *11.07 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
 
Theoremsb6a 1741* Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
 
Theorem2sb5rf 1742* Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
   &       =>   
 
Theorem2sb6rf 1743* Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
   &       =>   
 
Theoremdfsb7 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.)
 
Theoremsb7f 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.)
   =>   
 
Theoremsb7af 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.)

 F/   =>   
 
Theoremdfsb7a 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  F/ rather than and being distinct, see sb7af 1746. (Contributed by Jim Kingdon, 5-Feb-2018.)
 
Theoremsb10f 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.)
   =>   
 
Theoremsbid2v 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.)
 
Theoremsbelx 1750* Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
 
Theoremsbel2x 1751* Elimination of double substitution. (Contributed by NM, 5-Aug-1993.)
 
Theoremsbalyz 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.)
 
Theoremsbal 1753* Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
 
Theoremsbal1yz 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.)
 
Theoremsbal1 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.)
 
Theoremsbexyz 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.)
 
Theoremsbex 1757* Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
 
Theoremsbalv 1758* Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
   =>   
 
Theoremexsb 1759* An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
 
Theorem2exsb 1760* An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.)
 
TheoremdvelimALT 1761* Version of dvelim 1768 that doesn't use ax-10 1329. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.)
   &       =>   
 
Theoremdvelimfv 1762* Like dvelimf 1766 but with a distinct variable constraint on and . (Contributed by Jim Kingdon, 6-Mar-2018.)
   &       &       =>   
 
Theoremhbsb4 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.)
   =>   
 
Theoremhbsb4t 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.)
 
Theoremnfsb4t 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.)
 F/  F/
 
Theoremdvelimf 1766 Version of dvelim 1768 without any variable restrictions. (Contributed by NM, 1-Oct-2002.)
   &       &       =>   
 
Theoremdvelimdf 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.)

 F/   &     F/   &     F/   &     F/   &       =>     F/
 
Theoremdvelim 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.)

   &       =>   
 
Theoremdvelimor 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.)

 F/   &       =>     F/
 
Theoremdveeq1 1770* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.)
 
Theoremdveel1 1771* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
 
Theoremdveel2 1772* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
 
Theoremsbal2 1773* Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.)
 
Theoremnfsb4or 1774 A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.)

 F/   =>     F/
 
PART 2  SET THEORY

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).

 
2.1  IZF Set Theory - start with the Axiom of Extensionality
 
2.1.1  Introduce the Axiom of Extensionality
 
Axiomax-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.)

 
Theoremaxext3 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.)
 
Theoremaxext4 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.)
 
2.1.2  Class abstractions (a.k.a. class builders)
 
Syntaxcab 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.
 {  |  }
 
Definitiondf-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.)

 {  |  }
 
Theoremabid 1780 Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.)
 {  |  }
 
Theoremhbab1 1781* Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 5-Aug-1993.)
 {  |  }  {  |  }
 
Theoremnfsab1 1782* Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/ 
 {  |  }
 
Theoremhbab 1783* Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 1-Mar-1995.)
   =>     {  |  }  {  |  }
 
Theoremnfsab 1784* Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/   =>    
 F/ 
 {  |  }
 
Definitiondf-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.)

   =>   
 
Theoremdfcleq 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.)
 
Theoremcvjust 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.)
 {  |  }
 
Definitiondf-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.)

 
Theoremeqriv 1789* Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremeqrdv 1790* Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
   =>   
 
Theoremeqrdav 1791* Deduce equality of classes from an equivalence of membership that depends on the membership variable. (Contributed by NM, 7-Nov-2008.)
 C   &     C   &     C    =>   
 
Theoremeqid 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.)

 
Theoremeqidd 1793 Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)
 
Theoremeqcom 1794 Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
 
Theoremeqcoms 1795 Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremeqcomi 1796 Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremeqcomd 1797 Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
   =>   
 
Theoremeqeq1 1798 Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
 C  C
 
Theoremeqeq1i 1799 Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
   =>     C  C
 
Theoremeqeq1d 1800 Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
   =>     C  C
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2186
  Copyright terms: Public domain < Previous  Next >