mmtheorems14 - 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-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 1301-1400 - Page 14 of 123

Type	Label	Description
Statement
Theorem	sb9i 1301	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph -> A.y[y / x]ph)
Theorem	sb9 1302	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph <-> A.y[y / x]ph)
Predicate calculus with distinct variables (cont.)
Theorem	ax11v 1303	This is a version of ax-11o 1255 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See theorem ax11v2 1252 for the rederivation of ax-11o 1255 from this theorem.
|- (x = y -> (ph -> A.x(x = y -> ph)))
Theorem	sb56 1304	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 1209.
|- (E.x(x = y /\ ph) <-> A.x(x = y -> ph))
Theorem	sb6 1305	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))
Theorem	sb5 1306	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40.
|- ([y / x]ph <-> E.x(x = y /\ ph))
Theorem	equid1 1307	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This proof is similar to Tarski's and makes use of a dummy variable y. See equid 1162 for a proof that avoids dummy variables (but is less intuitive).
|- x = x
Theorem	ax16i 1308	Inference with ax-16 1247 as its conclusion, that doesn't require ax-10 1002, ax-11 1003, or ax-12 1004 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases.
|- (x = z -> (ph <-> ps))   &   |- (ps -> A.xps)   =>   |- (A.x x = y -> (ph -> A.xph))
Theorem	ax16ALT 1309	Version of ax16 1246 that doesn't require ax-10 1002 or ax-12 1004 for its proof.
|- (A.x x = y -> (ph -> A.xph))
Theorem	a4v 1310	Specialization, using implicit substitition.
|- (x = y -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	a4imev 1311	Distinct-variable version of a4ime 1197.
|- (x = y -> (ph -> ps))   =>   |- (ph -> E.xps)
Theorem	a4eiv 1312	Inference from existential specialization, using implicit substitition.
|- (x = y -> (ph <-> ps))   &   |- ps   =>   |- E.xph
Theorem	equvin 1313	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
|- (x = y <-> E.z(x = z /\ z = y))
Theorem	a16g 1314	A generalization of axiom ax-16 1247.
|- (A.x x = y -> (ph -> A.zph))
Theorem	a16gb 1315	A generalization of axiom ax-16 1247.
|- (A.x x = y -> (ph <-> A.zph))
Theorem	albidv 1316	Formula-building rule for universal quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	exbidv 1317	Formula-building rule for existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	2albidv 1318	Formula-building rule for 2 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xA.yps <-> A.xA.ych))
Theorem	2exbidv 1319	Formula-building rule for 2 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yps <-> E.xE.ych))
Theorem	3exbidv 1320	Formula-building rule for 3 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yE.zps <-> E.xE.yE.zch))
Theorem	4exbidv 1321	Formula-building rule for 4 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yE.zE.wps <-> E.xE.yE.zE.wch))
Theorem	19.9v 1322	Special case of Theorem 19.9 of [Margaris] p. 89.
|- (E.xph <-> ph)
Theorem	19.21v 1323	Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (ph -> A.xph) in 19.21 1092 via the use of distinct variable conditions combined with ax-17 1007. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 1423 derived from df-eu 1421. The "f" stands for "not free in" which is less restrictive than "does not occur in."
|- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	19.21aiv 1324	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	19.21aivv 1325	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (ph -> A.xA.yps)
Theorem	19.21adv 1326	Deduction from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	19.20dv 1327	Deduction from Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))
Theorem	19.22dv 1328	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	19.20dvv 1329	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xA.yps -> A.xA.ych))
Theorem	19.22dvv 1330	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xE.yps -> E.xE.ych))
Theorem	19.23v 1331	Special case of Theorem 19.23 of [Margaris] p. 90.
|- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23vv 1332	Theorem 19.23 of [Margaris] p. 90 extended to two variables.
|- (A.xA.y(ph -> ps) <-> (E.xE.yph -> ps))
Theorem	19.23aiv 1333	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23aivv 1334	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (E.xE.yph -> ps)
Theorem	19.23advv 1335	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xE.yps -> ch))
Theorem	19.27v 1336	Theorem 19.27 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28v 1337	Theorem 19.28 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.36v 1338	Special case of Theorem 19.36 of [Margaris] p. 90.
|- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36aiv 1339	Inference from Theorem 19.36 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.12vv 1340	Special case of 19.12 1083 where its converse holds.
|- (E.xA.y(ph -> ps) <-> A.yE.x(ph -> ps))
Theorem	19.37v 1341	Special case of Theorem 19.37 of [Margaris] p. 90.
|- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.37aiv 1342	Inference from Theorem 19.37 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (ph -> E.xps)
Theorem	19.41v 1343	Special case of Theorem 19.41 of [Margaris] p. 90.
|- (E.x(ph /\ ps) <-> (E.xph /\ ps))
Theorem	19.41vv 1344	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers.
|- (E.xE.y(ph /\ ps) <-> (E.xE.yph /\ ps))
Theorem	19.41vvv 1345	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers.
|- (E.xE.yE.z(ph /\ ps) <-> (E.xE.yE.zph /\ ps))
Theorem	19.42v 1346	Special case of Theorem 19.42 of [Margaris] p. 90.
|- (E.x(ph /\ ps) <-> (ph /\ E.xps))
Theorem	exdistr 1347	Distribution of existential quantifiers.
|- (E.xE.y(ph /\ ps) <-> E.x(ph /\ E.yps))
Theorem	19.42vv 1348	Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers.
|- (E.xE.y(ph /\ ps) <-> (ph /\ E.xE.yps))
Theorem	exdistr2 1349	Distribution of existential quantifiers.
|- (E.xE.yE.z(ph /\ ps) <-> E.x(ph /\ E.yE.zps))
Theorem	3exdistr 1350	Distribution of existential quantifiers.
|- (E.xE.yE.z(ph /\ ps /\ ch) <-> E.x(ph /\ E.y(ps /\ E.zch)))
Theorem	4exdistr 1351	Distribution of existential quantifiers.
|- (E.xE.yE.zE.w((ph /\ ps) /\ (ch /\ th)) <-> E.x(ph /\ E.y(ps /\ E.z(ch /\ E.wth))))
Theorem	cbvalv 1352	Rule used to change bound variables, using implicit substitition.
|- (x = y -> (ph <-> ps))   =>   |- (A.xph <-> A.yps)
Theorem	cbvexv 1353	Rule used to change bound variables, using implicit substitition.
|- (x = y -> (ph <-> ps))   =>   |- (E.xph <-> E.yps)
Theorem	cbval2 1354	Rule used to change bound variables, using implicit substitition.
|- (ph -> A.zph)   &   |- (ph -> A.wph)   &   |- (ps -> A.xps)   &   |- (ps -> A.yps)   &   |- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- (A.xA.yph <-> A.zA.wps)
Theorem	cbvex2 1355	Rule used to change bound variables, using implicit substitition.
|- (ph -> A.zph)   &   |- (ph -> A.wph)   &   |- (ps -> A.xps)   &   |- (ps -> A.yps)   &   |- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- (E.xE.yph <-> E.zE.wps)
Theorem	cbval2v 1356	Rule used to change bound variables, using implicit substitition.
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- (A.xA.yph <-> A.zA.wps)
Theorem	cbvex2v 1357	Rule used to change bound variables, using implicit substitition.
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- (E.xE.yph <-> E.zE.wps)
Theorem	cbvald 1358	Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1391.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.yps))   &   |- (ph -> (x = y -> (ps <-> ch)))   =>   |- (ph -> (A.xps <-> A.ych))
Theorem	cbvexd 1359	Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1391.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.yps))   &   |- (ph -> (x = y -> (ps <-> ch)))   =>   |- (ph -> (E.xps <-> E.ych))
Theorem	cbvex4v 1360	Rule used to change bound variables, using implicit substitition.
|- ((x = v /\ y = u) -> (ph <-> ps))   &   |- ((z = f /\ w = g) -> (ps <-> ch))   =>   |- (E.xE.yE.zE.wph <-> E.vE.uE.fE.gch)
Theorem	eeanv 1361	Rearrange existential quantifiers.
|- (E.xE.y(ph /\ ps) <-> (E.xph /\ E.yps))
Theorem	eeeanv 1362	Rearrange existential quantifiers.
|- (E.xE.yE.z(ph /\ ps /\ ch) <-> (E.xph /\ E.yps /\ E.zch))
Theorem	ee4anv 1363	Rearrange existential quantifiers.
|- (E.xE.yE.zE.w(ph /\ ps) <-> (E.xE.yph /\ E.zE.wps))
Theorem	nexdv 1364	Deduction for generalization rule for negated wff.
|- (ph -> -. ps)   =>   |- (ph -> -. E.xps)
Theorem	chvarv 1365	Implicit substitution of y for x into a theorem.
|- (x = y -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	cleljust 1366	When the class variables in definition df-clel 1514 are replaced with set variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the set variables in wel 995 with the class variables in wcel 994.
|- (x e. y <-> E.z(z = x /\ z e. y))
More substitution theorems
Theorem	sbhb 1367	Two ways of expressing "x is not free in ph".
|- ((ph -> A.xph) <-> A.y(ph -> [y / x]ph))
Theorem	equsb3lem 1368	Lemma for equsb3 1369.
Theorem	equsb3 1369	Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.)
|- ([x / y]y = z <-> x = z)
Theorem	elsb3 1370	Substitution applied to an atomic membership wff.
|- ([x / y]y e. z <-> x e. z)
Theorem	hbs1 1371	x is not free in [y / x]ph when x and y are distinct.
|- ([y / x]ph -> A.x[y / x]ph)
Theorem	hbsb 1372	If z is not free in ph, it is not free in [y / x]ph when y and z are distinct.
|- (ph -> A.zph)   =>   |- ([y / x]ph -> A.z[y / x]ph)
Theorem	sbcom2 1373	Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint).
|- ([w / z][y / x]ph <-> [y / x][w / z]ph)
Theorem	2sb5 1374	Equivalence for double substitution.
|- ([z / x][w / y]ph <-> E.xE.y((x = z /\ y = w) /\ ph))
Theorem	2sb6 1375	Equivalence for double substitution.
|- ([z / x][w / y]ph <-> A.xA.y((x = z /\ y = w) -> ph))
Theorem	sb6a 1376	Equivalence for substitution.
|- ([y / x]ph <-> A.x(x = y -> [x / y]ph))
Theorem	2sb5rf 1377	Reversed double substitution.
|- (ph -> A.zph)   &   |- (ph -> A.wph)   =>   |- (ph <-> E.zE.w((z = x /\ w = y) /\ [z / x][w / y]ph))
Theorem	2sb6rf 1378	Reversed double substitution.
|- (ph -> A.zph)   &   |- (ph -> A.wph)   =>   |- (ph <-> A.zA.w((z = x /\ w = y) -> [z / x][w / y]ph))
Theorem	dfsb7 1379	An alternate definition of proper substitution df-sb 1209. By introducing a dummy variable z in the definiens, we are able to eliminate any distinct variable restrictions among the variables x, y, and ph of the definiendum. No distinct variable conflicts arise because z effectively insulates x from y. To achieve this, we use a chain of two substitutions in the form of sb5 1306, first z for x then y for z. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 1506. Theorem sb7f 1380 provides a version where ph and z don't have to be distinct.
|- ([y / x]ph <-> E.z(z = y /\ E.x(x = z /\ ph)))
Theorem	sb7f 1380	This version of dfsb7 1379 does not require that ph and z be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1007 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1209 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.)
|- (ph -> A.zph)   =>   |- ([y / x]ph <-> E.z(z = y /\ E.x(x = z /\ ph)))
Theorem	sb10f 1381	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.
|- (ph -> A.xph)   =>   |- ([y / z]ph <-> E.x(x = y /\ [x / z]ph))
Theorem	sbid2v 1382	An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint).
|- ([y / x][x / y]ph <-> ph)
Theorem	sbelx 1383	Elimination of substitution.
|- (ph <-> E.x(x = y /\ [x / y]ph))
Theorem	sbel2x 1384	Elimination of double substitution.
|- (ph <-> E.xE.y((x = z /\ y = w) /\ [y / w][x / z]ph))
Theorem	sbal1 1385	A theorem used in elimination of disjoint variable restriction on x and y by replacing it with a distinctor -. A.xx = z.
|- (-. A.x x = z -> ([z / y]A.xph <-> A.x[z / y]ph))
Theorem	sbal 1386	Move universal quantifier in and out of substitution.
|- ([z / y]A.xph <-> A.x[z / y]ph)
Theorem	sbex 1387	Move existential quantifier in and out of substitution.
|- ([z / y]E.xph <-> E.x[z / y]ph)
Theorem	sbalv 1388	Quantify with new variable inside substitution.
|- ([y / x]ph <-> ps)   =>   |- ([y / x]A.zph <-> A.zps)
Theorem	exsb 1389	An equivalent expression for existence.
|- (E.xph <-> E.yA.x(x = y -> ph))
Theorem	2exsb 1390	An equivalent expression for double existence.
|- (E.xE.yph <-> E.zE.wA.xA.y((x = z /\ y = w) -> ph))
Theorem	dvelim 1391	This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -. A.xx = y as an antecedent. ph normally has z free and can be read ph(z), and ps substitutes y for z and can be read ph(y). We don't require that x and y 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 A.xA.z, conjoin them, and apply dvelimdf 1289.
|- (ph -> A.xph)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	dvelimALT 1392	Version of dvelim 1391 that doesn't use ax-10 1002. (See dvelimfALT 1190 for a version that doesn't use ax-11 1003.)
|- (ph -> A.xph)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	dveeq1 1393	Quantifier introduction when one pair of variables is distinct.
|- (-. A.x x = y -> (y = z -> A.x y = z))
Theorem	dveeq1ALT 1394	Version of dveeq1 1393 using ax-16 1247 instead of ax-17 1007.
|- (-. A.x x = y -> (y = z -> A.x y = z))
Theorem	dveel1 1395	Quantifier introduction when one pair of variables is distinct.
|- (-. A.x x = y -> (y e. z -> A.x y e. z))
Theorem	dveel2 1396	Quantifier introduction when one pair of variables is distinct.
|- (-. A.x x = y -> (z e. y -> A.x z e. y))
Theorem	sbal2 1397	Move quantifier in and out of substitution.
|- (-. A.x x = y -> ([z / y]A.xph <-> A.x[z / y]ph))
Theorem	ax15 1398	Axiom ax-15 1399 is redundant if we assume ax-17 1007. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'. Note that w is a dummy variable introduced in the proof. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 1396 and ax-17 1007. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. This theorem should not be referenced in any proof. Instead, use ax-15 1399 below so that theorems needing ax-15 1399 can be more easily identified.
|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
Axiom	ax-15 1399	Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 1007; see theorem ax15 1398. Alternately, ax-17 1007 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1007. We retain ax-15 1399 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1007, which 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	ax17el 1400	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-17 1007 considered as a metatheorem.)
|- (x e. y -> A.z x e. y)