Metamath Proof Explorer - mmtheorems9

Jump to page: 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-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 801-900 - Page 9 of 58

Type	Label	Description
Statement
Axiom	ax-11 801	Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The antecedent becomes false if the same variable is substituted for x and y, ensuring the axiom is sound whenever this is the case. The final consequent A.x(x = y -> ph) is a way of expressing "y substituted for x in wff ph". Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Axiom C8 of [Monk2] p. 105, from which it is easily proved by cases. To understand this easier, think of -. A.xx = y ->... as an informal equivalent for "if x and y are distinct variables then..." In some later theorems we call an antecedent of the form -. A.xx = y a "distinctor".
|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
Axiom	ax-12 802	Axiom of Quantifier Introduction. One of the 5 equality axioms of predicate calculus. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases.
|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
Syntax	wel 803	Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "x is an element of y," "x is a member of y," "x belongs to y," or "y contains x." Note: The phrase "y includes x" means "x is a subset of y"; to use it also for x e. y (as some authors occasionally do) is poor form and causes confusion.
wff x e. y
Axiom	ax-13 804	Axiom of Equality. One of the 3 non-logical predicate axioms of our predicate calculus. It substitutes equal variables into the left-hand side of the e. binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments.
|- (x = y -> (x e. z -> y e. z))
Axiom	ax-14 805	Axiom of Equality. One of the 3 non-logical predicate axioms of our predicate calculus. It substitutes equal variables into the right-hand side of the e. binary predicate. Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77.
|- (x = y -> (z e. x -> z e. y))
Axiom	ax-15 806	Axiom of Quantifier Introduction. One of the 3 non-logical predicate axioms of our predicate calculus. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 925; see theorem ax15 1006 below. Alternately, ax-17 925 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic provided by ax-17 925. We retain ax-15 806 here to provide completeness for systems with the simpler metalogic afforded by omitting ax-17 925, that might be easier to study for some theoretical purposes.
|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
Theorem	ax9 807	This is a variant of ax-9 799. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint).
|- (A.x(x = y -> A.xph) -> ph)
Theorem	ax9a 808	This theorem is a re-derivation of ax-9 799 from ax9 807. This shows that ax-9 799 and ax9 807 are interchangeable in the presence of the other axioms. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). Use it instead of ax-9 799 so we interchange ax-9 799 and ax9 807 as our axiom.
|- -. A.x -. x = y
Theorem	a9e 809	At least one individual exists.
|- E.x x = y
Theorem	eqid 810	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof is not as obvious as you might think.) This proof uses only axioms without distinct variable conditions and thus involves no dummy variables. A shorter proof, similar to Tarki's, is possible if we make use of ax-17 925; see the proof of x = x on the Metamath Solitaire page.
|- x = x
Theorem	eqcom 811	Commutative law for equality. Lemma 7 of [Tarski] p. 69.
|- (x = y -> y = x)
Theorem	eqcomb 812	Commutative law for equality.
|- (x = y <-> y = x)
Theorem	eqcoms 813	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.
|- (x = y -> ph)   =>   |- (y = x -> ph)
Theorem	eqt 814	A transitive law for equality.
|- (x = y -> (y = z -> x = z))
Theorem	eqt2 815	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint).
|- (x = y -> (z = x -> z = y))
Theorem	eqan 816	A transitive law for equality.
|- ((x = z /\ y = z) -> x = y)
Theorem	a8b 817	An equivalence law for equality.
|- (x = y -> (x = z <-> y = z))
Theorem	eqt2b 818	An equivalence law for equality.
|- (x = y -> (z = x <-> z = y))
Theorem	a13b 819	An identity law for the non-logical predicate.
|- (x = y -> (x e. z <-> y e. z))
Theorem	a14b 820	An identity law for the non-logical predicate.
|- (x = y -> (z e. x <-> z e. y))
Theorem	eq4 821	Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable.
|- (A.x x = y -> A.y y = x)
Theorem	eq4s 822	A commutation rule for identical variable specifiers.
|- (A.x x = y -> ph)   =>   |- (A.y y = x -> ph)
Theorem	eq4ds 823	A commutation rule for distinct variable specifiers.
|- (-. A.x x = y -> ph)   =>   |- (-. A.y y = x -> ph)
Theorem	eq5 824	All variables are effectively bound in an identical variable specifier.
|- (A.x x = y -> A.zA.x x = y)
Theorem	eq5s 825	Rule that applies eq5 824 to antecedent.
|- (A.zA.x x = y -> ph)   =>   |- (A.x x = y -> ph)
Theorem	eq6 826	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint).
|- (-. A.x x = y -> A.z -. A.x x = y)
Theorem	eq6s 827	Rule that applies eq6 826 to antecedent.
|- (A.z -. A.x x = y -> ph)   =>   |- (-. A.x x = y -> ph)
Theorem	eqs1 828	Lemma used in proofs of substitution properties.
|- (A.x(x = y -> ph) -> -. A.x(x = y -> -. ph))
Theorem	eqs2 829	Lemma used in proofs of substitution properties.
|- (-. A.x x = y -> (-. A.x(x = y -> -. ph) -> A.x(x = y -> ph)))
Theorem	eqs3 830	Lemma used in proofs of substitution properties.
|- (E.x(x = y /\ ph) <-> -. A.x(x = y -> -. ph))
Theorem	eqs4 831	Lemma used in proofs of substitution properties.
|- (A.x(x = y -> ph) -> E.x(x = y /\ ph))
Theorem	eqs5 832	Lemma used in proofs of substitution properties.
|- (-. A.x x = y -> (E.x(x = y /\ ph) -> A.x(x = y -> ph)))
Theorem	eqsal 833	A useful equivalence related to substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x(x = y -> ph) <-> ps)
Theorem	eqsex 834	A useful equivalence related to substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x(x = y /\ ph) <-> ps)
Theorem	del34 835	A distinctor elimination lemma. Formula-builder for universal quantifier.
|- (A.x x = y -> (ph -> ps))   =>   |- (A.x x = y -> (A.xph -> A.yps))
Theorem	del35 836	A distinctor elimination lemma. Formula-builder for universal quantifier.
|- (A.x x = y -> (ph -> ps))   =>   |- (A.x x = y -> (A.yph -> A.xps))
Theorem	del34b 837	A distinctor elimination lemma. Formula-builder for universal quantifier.
|- (A.x x = y -> (ph <-> ps))   =>   |- (A.x x = y -> (A.xph <-> A.yps))
Theorem	del36 838	A distinctor elimination lemma. Formula-builder for universal quantifier.
|- (A.x x = y -> (ph -> ps))   =>   |- (A.x x = y -> (A.zph -> A.zps))
Theorem	del40 839	A distinctor elimination lemma. Formula-builder for existential quantifier.
|- (A.x x = y -> (ph -> ps))   =>   |- (A.x x = y -> (E.xph -> E.yps))
Theorem	del41 840	A distinctor elimination lemma. Formula-builder for existential quantifier.
|- (A.x x = y -> (ph -> ps))   =>   |- (A.x x = y -> (E.yph -> E.xps))
Theorem	del42 841	A distinctor elimination lemma. Formula-builder for existential quantifier.
|- (A.x x = y -> (ph -> ps))   =>   |- (A.x x = y -> (E.zph -> E.zps))
Theorem	a4a 842	Specialization with implicit substitution. Compare Lemma 14 of [Tarski] p. 70.
|- (ps -> A.xps)   &   |- (x = y -> (ph -> ps))   =>   |- (A.xph -> ps)
Theorem	a4c 843	Existential introduction with implicit substitution. Compare Lemma 14 of [Tarski] p. 70.
|- (ph -> A.xph)   &   |- (x = y -> (ph -> ps))   =>   |- (ph -> E.xps)
Theorem	a4c1 844	A more general version of a4c 843.
|- (ch -> A.xch)   &   |- (ch -> (ph -> A.xph))   &   |- (x = y -> (ph -> ps))   =>   |- (ch -> (ph -> E.xps))
Theorem	cbv1 845	Rule used to change bound variables with implicit substitution.
|- (ph -> (ps -> A.yps))   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (x = y -> (ps -> ch)))   =>   |- (A.xA.yph -> (A.xps -> A.ych))
Theorem	cbv2 846	Rule used to change bound variables with implicit substitution.
|- (ph -> (ps -> A.yps))   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (x = y -> (ps <-> ch)))   =>   |- (A.xA.yph -> (A.xps <-> A.ych))
Theorem	cbv3 847	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph -> ps))   =>   |- (A.xph -> A.yps)
Theorem	cbval 848	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.xph <-> A.yps)
Theorem	cbvex 849	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.xph <-> E.yps)
Theorem	chv2 850	Implicit substitution of y for x into a theorem. (Contributed by Raph Levien, 9-Jul-03.)
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	eqvin.l1 851	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require z to be distinct from x and y (making the proof longer).
|- (x = y -> E.z(x = z /\ z = y))
Syntax	wsb 852	Extend wff definition to include proper substitution (read "the wff that results when y is properly substituted for x in wff ph").
wff [y / x]ph
Definition	df-sb 853	Define proper substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). For our notation, we use [y / x]ph to mean "the wff that results when y is properly substituted for x in the wff ph." This notation was introduced in Haskell B. Curry's Foundations of Mathematical Logic (1977), p. 316 and is frequently used in textbooks of lambda calculus and combinatory logic. This notation improves the common but ambiguous notation, "ph(y) is the wff that results when y is properly substituted for x in ph(x)". For example, if the original ph(x) is x = y, then ph(y) is y = y, from which we obtain that ph(x) is x = x. So what exactly does ph(x) mean? Curry's notation solves this problem. In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead we use a remarkable little formula that is exactly equivalent and gives us a single direct definition. We later prove that our definition has the properties we expect of proper substitution (see theorems sbequ 877, sbcom2 992 and sbid2v 993). Note that our definition is valid even when x and y are replaced with the same variable, as sbid 868 shows. We achieve this by having x free in the first conjunct and bound in the second. We can also achieve this by using a dummy variable, as the alternate definition sb7 991 shows (which some logicians may prefer because it doesn't mix free and bound variables). When x and y are distinct, we can express proper substitution with the simpler expressions of sb5 988 and sb6 989. There are no restrictions on what variables may occur in ph.
|- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
Theorem	sbimi 854	Infer substitution into antecedent and consequent of an implication.
|- (ph -> ps)   =>   |- ([y / x]ph -> [y / x]ps)
Theorem	bisb 855	Infer substitution into both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ([y / x]ph <-> [y / x]ps)
Theorem	del43 856	A distinctor elimination lemma for substitution.
|- (A.x x = y -> ([z / x]ph -> [z / y]ph))
Theorem	del43b 857	A distinctor elimination lemma for substitution.
|- (A.x x = y -> ([z / x]ph <-> [z / y]ph))
Theorem	sb1 858	One direction of a simplified definition of substitution.
|- ([y / x]ph -> E.x(x = y /\ ph))
Theorem	sb2 859	One direction of a simplified definition of substitution.
|-