mmtheorems13 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

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-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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10766

Color key:

Metamath Proof Explorer
(1-8795)

Hilbert Space Explorer
(8796-10377)

User Sandboxes
(10378-10766)

**Statement List for Metamath Proof Explorer -** 1201-1300 - Page 13 of 108
Type	Label	Description
Statement

Theorem	equs5e 1201	A property related to substitution that unlike equs5 1224 doesn't require a distinctor antecedent.
$/\$

Theorem	sb4a 1202	A version of sb4 1226 that doesn't require a distinctor antecedent.


Theorem	equs45f 1203	Two ways of expressing substitution when is not free in .
$/\$

Theorem	sb6f 1204	Equivalence for substitution when is not free in .


Theorem	sb5f 1205	Equivalence for substitution when is not free in .
$/\$

Theorem	sb4e 1206	One direction of a simplified definition of substitution that unlike sb4 1226 doesn't require a distinctor antecedent.


Theorem	hbsb2a 1207	Special case of a bound-variable hypothesis builder for substitution.


Theorem	hbsb2e 1208	Special case of a bound-variable hypothesis builder for substitution.


Theorem	hbsb3 1209	If is not free in , is not free in .


Predicate calculus with distinct variables

The axiom of quantifier introduction ax-17

Theorem	a4imv 1210	A version of a4im 1162 with a distinct variable requirement instead of a bound variable hypothesis.


Theorem	aev 1211	A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1213. The proof is unusual in that it involves linking 17 implications, which might provide an interesting challenge for an automated theorem prover.


Derive the axiom of distinct variables ax-16

Theorem	ax16 1212	Theorem showing that ax-16 1213 is redundant if ax-17 974 is included in the axiom system. The important part of the proof is provided by aev 1211. See ax16ALT 1274 for an alternate proof that does not require ax-10 969 or ax-12 971. This theorem should not be referenced in any proof. Instead, use ax-16 1213 below so that theorems needing ax-16 1213 can be more easily identified.


Axiom	ax-16 1213	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 974 to be a metatheorem and not an axiom). Axiom scheme C16' 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. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 2781), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-17 974; see theorem ax16 1212. Alternately, ax-17 974 becomes logically redundant in the presence of this axiom, but without ax-17 974 we lose the more powerful metalogic that results from being able to express the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). We retain ax-16 1213 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-17 974, which might be easier to study for some theoretical purposes.


Theorem	ax17eq 1214	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-17 974 considered as a metatheorem. Do not use it for later proofs - use ax-17 974 instead, to avoid reference to the redundant axiom ax-16 1213.)


Theorem	dveeq2 1215	Quantifier introduction when one pair of variables is distinct.


Theorem	dveeq2ALT 1216	Version of dveeq2 1215 using ax-16 1213 instead of ax-17 974.


Theorem	19.23adv 1217	Deduction from Theorem 19.23 of [Margaris] p. 90.


Theorem	ax11v2 1218	Recovery of ax11o 1220 from ax11v 1268 without using ax-11 970. The hypothesis is even weaker than ax11v 1268, with both distinct from and not occurring in . Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1220.


Theorem	ax11a2 1219	Derive ax-11o 1221 from a hypothesis in the form of ax-11 970. The hypothesis is even weaker than ax-11 970, with both distinct from and not occurring in . Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1220. As theorem ax11 1222 shows, the distinct variable conditions are optional. An open problem is whether ax11o 1220 can be derived from ax-11 970 without relying on ax-17 974.


Derive the original axiom of variable substitution ax-11o

Theorem	ax11o 1220	Derivation of set.mm's original ax-11o 1221 from the shorter ax-11 970 that has replaced it. An open problem is whether this theorem can be proved without relying on ax-16 1213 or ax-17 974. Another open problem is whether this theorem can be proved without relying on ax-12 971 (see note in a12study 1381). Theorem ax11 1222 shows the reverse derivation of ax-11 970 from ax-11o 1221. This theorem should not be referenced in any proof. Instead, use ax-11o 1221 below so that theorems needing ax-11o 1221 can be more easily identified.


Axiom	ax-11o 1221	Axiom ax-11o 1221 ("o" for "old") was the original version of ax-11 970, before it was discovered (in Jan. 2007) that the shorter ax-11 970 could replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. To understand this theorem more easily, think of " ..." as informally meaning "if and are distinct variables then..." The antecedent becomes false if the same variable is substituted for and , ensuring the theorem is sound whenever this is the case. In some later theorems, we call an antecedent of the form a "distinctor." This axiom is redundant, as shown by theorem ax11o 1220.


Theorem	ax11 1222	Rederivation of axiom ax-11 970 from the orginal version, ax-11o 1221. See theorem ax11o 1220 for the derivation of ax-11o 1221 from ax-11 970. This theorem should not be referenced in any proof. Instead, use ax-11 970 above so that uses of ax-11 970 can be more easily identified.


Theorems without distinct variables that use axiom ax-11o

Theorem	ax11b 1223	A bidirectional version of ax-11o 1221.
$/\$

Theorem	equs5 1224	Lemma used in proofs of substitution properties.
$/\$

Theorem	sb3 1225	One direction of a simplified definition of substitution when variables are distinct.
$/\$

Theorem	sb4 1226	One direction of a simplified definition of substitution when variables are distinct.


Theorem	sb4b 1227	Simplified definition of substitution when variables are distinct.


Theorem	dfsb2 1228	An alternate definition of proper substitution that, like df-sb 1175, mixes free and bound variables to avoid distinct variable requirements.
$/\$ $\/$

Theorem	dfsb3 1229	An alternate definition of proper substitution df-sb 1175 that uses only primitive connectives (no defined terms) on the right-hand side.


Theorem	hbsb2 1230	Bound-variable hypothesis builder for substitution.


Theorem	sbequi 1231	An equality theorem for substitution.


Theorem	sbequ 1232	An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint).


Theorem	drsb2 1233	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).


Theorem	sbn 1234	Negation inside and outside of substitution are equivalent.


Theorem	sbi1 1235	Removal of implication from substitution.


Theorem	sbi2 1236	Introduction of implication into substitution.


Theorem	sbim 1237	Implication inside and outside of substitution are equivalent.


Theorem	sbor 1238	Logical OR inside and outside of substitution are equivalent.
$\/$ $\/$

Theorem	sb19.21 1239	Substitution with a variable not free in antecedent affects only the consequent.


Theorem	sban 1240	Conjunction inside and outside of a substitution are equivalent.
$/\$ $/\$

Theorem	sb3an 1241	Conjunction inside and outside of a substitution are equivalent.
$/\$ $/\$ $/\$ $/\$

Theorem	sbbi 1242	Equivalence inside and outside of a substitution are equivalent.


Theorem	sblbis 1243	Introduce left biconditional inside of a substitution.


Theorem	sbrbis 1244	Introduce right biconditional inside of a substitution.


Theorem	sbrbif 1245	Introduce right biconditional inside of a substitution.


Theorem	a4sbe 1246	A specialization theorem.


Theorem	a4sbim 1247	Specialization of implication.


Theorem	a4sbbi 1248	Specialization of biconditional.


Theorem	sbbid 1249	Deduction substituting both sides of a biconditional.


Theorem	sbequ8 1250	Elimination of equality from antecedent after substitution.


Theorem	hbsb4 1251	A variable not free remains so after substitution with a distinct variable.


Theorem	hbsb4t 1252	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1251).