mmtheorems13 - Metamath Proof Explorer

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

Statement List for Metamath Proof Explorer - 1201-1300 - Page 13 of 105

Type	Label	Description
Statement
Derive the original axiom of variable substitution ax-11o
Theorem	ax11o 1201	Derivation of set.mm's original ax-11o 1202 from the shorter ax-11 1180 that has replaced it. 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 "-. A.xx = y ->..." as informally meaning "if x and y are distinct variables then..." The antecedent becomes false if the same variable is substituted for x and y, ensuring the theorem is sound whenever this is the case. In some later theorems we call an antecedent of the form -. A.xx = y a "distinctor." An open problem is whether this theorem can be proved without relying on ax-16 1194 or ax-17 1190. Theorem ax11 1203 shows the reverse derivation of ax-11 1180 from ax-11o 1202.
|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
Axiom	ax-11o 1202	Axiom ax-11o 1202 ("o" for "old") was the original version of ax-11 1180, before it was discovered (in Jan. 2007) that the shorter ax-11 1180 could replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). As theorem ax11o 1201 shows, ax-11o 1202 can be derived from ax-11 1180 and the other axioms; conversely, theorem ax11 1203 shows that ax-11 1180 can be derived from ax-11o 1202 and the others. An open problem is whether ax-11o 1202 can be derived from ax-11 1180 and the others when ax-16 1194 and ax-17 1190 are omitted. See ax-11 1180, ax11o 1201, and ax11 1203 for additional remarks. If we wish to identify where this axiom is needed in the absence of ax-16 1194 and ax-17 1190, we can use it in place of all references to theorem ax11o 1201 in the theorems that follow.
|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
Theorem	ax11 1203	Rederivation of axiom ax-11 1180 from the orginal version, ax-11o 1202.
|- (x = y -> (A.yph -> A.x(x = y -> ph)))
Theorems without d.v. restrictions that rely on axiom ax-11o
Theorem	ax11b 1204	A bidirectional version of ax-11o 1202.
|- ((-. A.x x = y /\ x = y) -> (ph <-> A.x(x = y -> ph)))
Theorem	equs5 1205	Lemma used in proofs of substitution properties.
|- (-. A.x x = y -> (E.x(x = y /\ ph) -> A.x(x = y -> ph)))
Theorem	sb3 1206	One direction of a simplified definition of substitution when variables are distinct.
|- (-. A.x x = y -> (E.x(x = y /\ ph) -> [y / x]ph))
Theorem	sb4 1207	One direction of a simplified definition of substitution when variables are distinct.
|- (-. A.x x = y -> ([y / x]ph -> A.x(x = y -> ph)))
Theorem	sb4b 1208	Simplified definition of substitution when variables are distinct.
|- (-. A.x x = y -> ([y / x]ph <-> A.x(x = y -> ph)))
Theorem	dfsb2 1209	An alternate definition of proper substitution that, like df-sb 1155, mixes free and bound variables to avoid distinct variable requirements.
|- ([y / x]ph <-> ((x = y /\ ph) \/ A.x(x = y -> ph)))
Theorem	dfsb3 1210	An alternate definition of proper substitution df-sb 1155 that uses only primitive connectives (no defined terms) on the right-hand side.
|- ([y / x]ph <-> ((x = y -> -. ph) -> A.x(x = y -> ph)))
Theorem	hbsb2 1211	Bound-variable hypothesis builder for substitution.
|- (-. A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
Theorem	sbequi 1212	An equality theorem for substitution.
|- (x = y -> ([x / z]ph -> [y / z]ph))
Theorem	sbequ 1213	An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint).
|- (x = y -> ([x / z]ph <-> [y / z]ph))
Theorem	drsb2 1214	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
|- (A.x x = y -> ([x / z]ph <-> [y / z]ph))
Theorem	sbn 1215	Negation inside and outside of substitution are equivalent.
|- ([y / x] -. ph <-> -. [y / x]ph)
Theorem	sbi1 1216	Removal of implication from substitution.
|- ([y / x](ph -> ps) -> ([y / x]ph -> [y / x]ps))
Theorem	sbi2 1217	Introduction of implication into substitution.
|- (([y / x]ph -> [y / x]ps) -> [y / x](ph -> ps))
Theorem	sbim 1218	Implication inside and outside of substitution are equivalent.
|- ([y / x](ph -> ps) <-> ([y / x]ph -> [y / x]ps))
Theorem	sbor 1219	Logical OR inside and outside of substitution are equivalent.
|- ([y / x](ph \/ ps) <-> ([y / x]ph \/ [y / x]ps))
Theorem	sb19.21 1220	Substitution with a variable not free in antecedent affects only the consequent.
|- (ph -> A.xph)   =>   |- ([y / x](ph -> ps) <-> (ph -> [y / x]ps))
Theorem	sban 1221	Conjunction inside and outside of a substitution are equivalent.
|- ([y / x](ph /\ ps) <-> ([y / x]ph /\ [y / x]ps))
Theorem	sb3an 1222	Conjunction inside and outside of a substitution are equivalent.
|- ([y / x](ph /\ ps /\ ch) <-> ([y / x]ph /\ [y / x]ps /\ [y / x]ch))
Theorem	sbbi 1223	Equivalence inside and outside of a substitution are equivalent.
|- ([y / x](ph <-> ps) <-> ([y / x]ph <-> [y / x]ps))
Theorem	sblbis 1224	Introduce left biconditional inside of a substitution.
|- ([y / x]ph <-> ps)   =>   |- ([y / x](ch <-> ph) <-> ([y / x]ch <-> ps))
Theorem	sbrbis 1225	Introduce right biconditional inside of a substitution.
|- ([y / x]ph <-> ps)   =>   |- ([y / x](ph <-> ch) <-> (ps <-> [y / x]ch))
Theorem	sbrbif 1226	Introduce right biconditional inside of a substitution.
|- (ch -> A.xch)   &   |- ([y / x]ph <-> ps)   =>   |- ([y / x](ph <-> ch) <-> (ps <-> ch))
Theorem	sbea4 1227	A specialization theorem.
|- ([y / x]ph -> E.xph)
Theorem	sbia4 1228	Specialization of implication.
|- (A.x(ph -> ps) -> ([y / x]ph -> [y / x]ps))
Theorem	sbba4 1229	Specialization of biconditional.
|- (A.x(ph <-> ps) -> ([y / x]ph <-> [y / x]ps))
Theorem	sbbid 1230	Deduction substituting both sides of a biconditional.
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ([y / x]ps <-> [y / x]ch))
Theorem	sbequ8 1231	Elimination of equality from antecedent after substitution.
|- ([y / x]ph <-> [y / x](x = y -> ph))
Theorem	hbsb4 1232	A variable not free remains so after substitution with a distinct variable.
|- (ph -> A.zph)   =>   |- (-. A.z z = y -> ([y / x]ph -> A.z[y / x]ph))
Theorem	hbsb4t 1233	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1232).
|- (A.xA.z(ph -> A.zph) -> (-. A.z z = y -> ([y / x]ph -> A.z[y / x]ph)))
Theorem	dvelimf 1234	Version of dvelim 1334 without any variable restrictions.
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	dvelimdf 1235	Deduction form of dvelimf 1234. This version may be useful if we want to avoid ax-17 1190 and use ax-16 1194 instead.
|- (ph -> A.xph)   &   |- (ph -> A.zph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.zch))   &   |- (ph -> (z = y -> (ps <-> ch)))   =>   |- (ph -> (-. A.x x = y -> (ch -> A.xch)))
Theorem	sbco 1236	A composition law for substitution.
|- ([y / x][x / y]ph <-> [y / x]ph)
Theorem	sbid2 1237	An identity law for substitution.
|- (ph -> A.xph)   =>   |- ([y / x][x / y]ph <-> ph)
Theorem	sbidm 1238	An idempotent law for substitution.
|- ([y / x][y / x]ph <-> [y / x]ph)
Theorem	sbco2 1239	A composition law for substitution.
|- (ph -> A.zph)   =>   |- ([y / z][z / x]ph <-> [y / x]ph)
Theorem	sbco2d 1240	A composition law for substitution.
|- (ph -> A.xph)   &   |- (ph -> A.zph)   &   |- (ph -> (ps -> A.zps))   =>   |- (ph -> ([y / z][z / x]ps <-> [y / x]ps))
Theorem	sbco3 1241	A composition law for substitution.
|- ([z / y][y / x]ph <-> [z / x][x / y]ph)
Theorem	sbcom 1242	A commutativity law for substitution.
|- ([y / z][y / x]ph <-> [y / x][y / z]ph)
Theorem	sb5rf 1243	Reversed substitution.
|- (ph -> A.yph)   =>   |- (ph <-> E.y(y = x /\ [y / x]ph))
Theorem	sb6rf 1244	Reversed substitution.
|- (ph -> A.yph)   =>   |- (ph <-> A.y(y = x -> [y / x]ph))
Theorem	sb8 1245	Substitution of variable in universal quantifier.
|- (ph -> A.yph)   =>   |- (A.xph <-> A.y[y / x]ph)
Theorem	sb8e 1246	Substitution of variable in existential quantifier.
|- (ph -> A.yph)   =>   |- (E.xph <-> E.y[y / x]ph)
Theorem	sb9i 1247	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph -> A.y[y / x]ph)
Theorem	sb9 1248	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph <-> A.y[y / x]ph)
Predicate calculus with distinct variables (cont.)
Theorem	ax11v 1249	This is a version of ax-11o 1202 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See theorem ax11v2 1199 for the rederivation of ax-11o 1202 from this theorem.
|- (x = y -> (ph -> A.x(x = y -> ph)))
Theorem	sb56 1250	Two equivalent ways of expressing the proper substitution of y for x in ph, when x and y are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1155.
|- (E.x(x = y /\ ph) <-> A.x(x = y -> ph))
Theorem	sb6 1251	Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70.
|- ([y / x]ph <-> A.x(x = y -> ph))