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-10781

Color key:

Metamath Proof Explorer
(1-8787)

Hilbert Space Explorer
(8788-10368)

User Sandboxes
(10369-10781)

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

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


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

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


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


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


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


Predicate calculus with distinct variables

The axiom of quantifier introduction ax-17

Theorem	a4imv 1207	A version of a4im 1159 with a distinct variable requirement instead of a bound variable hypothesis.


Theorem	aev 1208	A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1210. 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 1209	Theorem showing that ax-16 1210 is redundant if ax-17 971 is included in the axiom system. The important part of the proof is provided by aev 1208. See ax16ALT 1271 for an alternate proof that does not require ax-10 966 or ax-12 968. This theorem should not be referenced in any proof. Instead, use ax-16 1210 below so that theorems needing ax-16 1210 can be more easily identified.


Axiom	ax-16 1210	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 971 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 2772), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-17 971; see theorem ax16 1209. Alternately, ax-17 971 becomes logically redundant in the presence of this axiom, but without ax-17 971 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 1210 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-17 971, which might be easier to study for some theoretical purposes.


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


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


Theorem	dveeq2ALT 1213	Version of dveeq2 1212 using ax-16 1210 instead of ax-17 971.


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


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


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


Derive the original axiom of variable substitution ax-11o

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


Axiom	ax-11o 1218	Axiom ax-11o 1218 ("o" for "old") was the original version of ax-11 967, before it was discovered (in Jan. 2007) that the shorter ax-11 967 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 1217.


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


Theorems without distinct variables that use axiom ax-11o

Theorem	ax11b 1220	A bidirectional version of ax-11o 1218.
$/\$

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

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

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


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


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

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


Theorem	hbsb2 1227	Bound-variable hypothesis builder for substitution.


Theorem	sbequi 1228	An equality theorem for substitution.


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


Theorem	drsb2 1230	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 1231	Negation inside and outside of substitution are equivalent.


Theorem	sbi1 1232	Removal of implication from substitution.


Theorem	sbi2 1233	Introduction of implication into substitution.


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


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

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


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

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

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


Theorem	sblbis 1240	Introduce left biconditional inside of a substitution.


Theorem	sbrbis 1241	Introduce right biconditional inside of a substitution.


Theorem	sbrbif 1242	Introduce right biconditional inside of a substitution.


Theorem	a4sbe 1243	A specialization theorem.


Theorem	a4sbim 1244	Specialization of implication.


Theorem	a4sbbi 1245	Specialization of biconditional.


Theorem	sbbid 1246	Deduction substituting both sides of a biconditional.


Theorem	sbequ8 1247	Elimination of equality from antecedent after substitution.


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


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


Theorem	dvelimf 1250	Version of dvelim 1352 without any variable restrictions.


Theorem	dvelimdf 1251	Deduction form of dvelimf 1250. This version may be useful if we want to avoid ax-17 971 and use ax-16 1210 instead.