mmtheorems17 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 1601-1700 - Page 17 of 175

Type	Label	Description
Statement
Theorem	sbn 1601	Negation inside and outside of substitution are equivalent.
|- ([y / x] -. ph <-> -. [y / x]ph)
Theorem	sbi1 1602	Removal of implication from substitution.
|- ([y / x](ph -> ps) -> ([y / x]ph -> [y / x]ps))
Theorem	sbi2 1603	Introduction of implication into substitution.
|- (([y / x]ph -> [y / x]ps) -> [y / x](ph -> ps))
Theorem	sbim 1604	Implication inside and outside of substitution are equivalent.
|- ([y / x](ph -> ps) <-> ([y / x]ph -> [y / x]ps))
Theorem	sbor 1605	Logical OR inside and outside of substitution are equivalent.
|- ([y / x](ph \/ ps) <-> ([y / x]ph \/ [y / x]ps))
Theorem	sb19.21 1606	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 1607	Conjunction inside and outside of a substitution are equivalent.
|- ([y / x](ph /\ ps) <-> ([y / x]ph /\ [y / x]ps))
Theorem	sb3an 1608	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 1609	Equivalence inside and outside of a substitution are equivalent.
|- ([y / x](ph <-> ps) <-> ([y / x]ph <-> [y / x]ps))
Theorem	sblbis 1610	Introduce left biconditional inside of a substitution.
|- ([y / x]ph <-> ps)   =>   |- ([y / x](ch <-> ph) <-> ([y / x]ch <-> ps))
Theorem	sbrbis 1611	Introduce right biconditional inside of a substitution.
|- ([y / x]ph <-> ps)   =>   |- ([y / x](ph <-> ch) <-> (ps <-> [y / x]ch))
Theorem	sbrbif 1612	Introduce right biconditional inside of a substitution.
|- (ch -> A.xch)   &   |- ([y / x]ph <-> ps)   =>   |- ([y / x](ph <-> ch) <-> (ps <-> ch))
Theorem	a4sbe 1613	A specialization theorem.
|- ([y / x]ph -> E.xph)
Theorem	a4sbim 1614	Specialization of implication. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (A.x(ph -> ps) -> ([y / x]ph -> [y / x]ps))
Theorem	a4sbimOLD 1615	Specialization of implication.
|- (A.x(ph -> ps) -> ([y / x]ph -> [y / x]ps))
Theorem	a4sbbi 1616	Specialization of biconditional.
|- (A.x(ph <-> ps) -> ([y / x]ph <-> [y / x]ps))
Theorem	sbbid 1617	Deduction substituting both sides of a biconditional.
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ([y / x]ps <-> [y / x]ch))
Theorem	sbequ8 1618	Elimination of equality from antecedent after substitution.
|- ([y / x]ph <-> [y / x](x = y -> ph))
Theorem	sbf3t 1619	Substitution has no effect on a non-free variable.
|- (A.x(ph -> A.xph) -> ([y / x]ph <-> ph))
Theorem	hbsb4 1620	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 1621	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1620). (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (A.xA.z(ph -> A.zph) -> (-. A.z z = y -> ([y / x]ph -> A.z[y / x]ph)))
Theorem	hbsb4tOLD 1622	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1620).
|- (A.xA.z(ph -> A.zph) -> (-. A.z z = y -> ([y / x]ph -> A.z[y / x]ph)))
Theorem	dvelimf 1623	Version of dvelim 1743 without any variable restrictions.
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	dvelimdf 1624	Deduction form of dvelimf 1623. This version may be useful if we want to avoid ax-17 1317 and use ax-16 1580 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 1625	A composition law for substitution.
|- ([y / x][x / y]ph <-> [y / x]ph)
Theorem	sbid2 1626	An identity law for substitution.
|- (ph -> A.xph)   =>   |- ([y / x][x / y]ph <-> ph)
Theorem	sbidm 1627	An idempotent law for substitution. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- ([y / x][y / x]ph <-> [y / x]ph)
Theorem	sbidmOLD 1628	An idempotent law for substitution.
|- ([y / x][y / x]ph <-> [y / x]ph)
Theorem	sbco2 1629	A composition law for substitution.
|- (ph -> A.zph)   =>   |- ([y / z][z / x]ph <-> [y / x]ph)
Theorem	sbco2d 1630	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 1631	A composition law for substitution.
|- ([z / y][y / x]ph <-> [z / x][x / y]ph)
Theorem	sbcom 1632	A commutativity law for substitution.
|- ([y / z][y / x]ph <-> [y / x][y / z]ph)
Theorem	sb5rf 1633	Reversed substitution. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> A.yph)   =>   |- (ph <-> E.y(y = x /\ [y / x]ph))
Theorem	sb5rfOLD 1634	Reversed substitution.
|- (ph -> A.yph)   =>   |- (ph <-> E.y(y = x /\ [y / x]ph))
Theorem	sb6rf 1635	Reversed substitution. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> A.yph)   =>   |- (ph <-> A.y(y = x -> [y / x]ph))
Theorem	sb6rfOLD 1636	Reversed substitution.
|- (ph -> A.yph)   =>   |- (ph <-> A.y(y = x -> [y / x]ph))
Theorem	sb8 1637	Substitution of variable in universal quantifier. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> A.yph)   =>   |- (A.xph <-> A.y[y / x]ph)
Theorem	sb8OLD 1638	Substitution of variable in universal quantifier.
|- (ph -> A.yph)   =>   |- (A.xph <-> A.y[y / x]ph)
Theorem	sb8e 1639	Substitution of variable in existential quantifier.
|- (ph -> A.yph)   =>   |- (E.xph <-> E.y[y / x]ph)
Theorem	sb9i 1640	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph -> A.y[y / x]ph)
Theorem	sb9 1641	Commutation of quantification and substitution variables.
|- (A.x[x / y]ph <-> A.y[y / x]ph)
Predicate calculus with distinct variables (cont.)
Theorem	ax11v 1642	This is a version of ax-11o 1588 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See theorem ax11v2 1585 for the rederivation of ax-11o 1588 from this theorem.
|- (x = y -> (ph -> A.x(x = y -> ph)))
Theorem	sb56 1643	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 1536.
|- (E.x(x = y /\ ph) <-> A.x(x = y -> ph))
Theorem	sb6 1644	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 1645	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40.
|- ([y / x]ph <-> E.x(x = y /\ ph))
Theorem	equid1 1646	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 1484 for a proof that avoids dummy variables (but is less intuitive).
|- x = x
Theorem	ax16i 1647	Inference with ax-16 1580 as its conclusion, that doesn't require ax-10 1308, ax-11 1309, or ax-12 1310 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 1648	Version of ax16 1579 that doesn't require ax-10 1308 or ax-12 1310 for its proof.
|- (A.x x = y -> (ph -> A.xph))
Theorem	a4v 1649	Specialization, using implicit substitition.
|- (x = y -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	a4imev 1650	Distinct-variable version of a4ime 1521.
|- (x = y -> (ph -> ps))   =>   |- (ph -> E.xps)
Theorem	a4eiv 1651	Inference from existential specialization, using implicit substitition.
|- (x = y -> (ph <-> ps))   &   |- ps   =>   |- E.xph
Theorem	equvin 1652	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
|- (x = y <-> E.z(x = z /\ z = y))
Theorem	a16g 1653	A generalization of axiom ax-16 1580. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (A.x x = y -> (ph -> A.zph))
Theorem	a16gOLD 1654	A generalization of axiom ax-16 1580.
|- (A.x x = y -> (ph -> A.zph))
Theorem	a16gb 1655	A generalization of axiom ax-16 1580.
|- (A.x x = y -> (ph <-> A.zph))
Theorem	albidv 1656	Formula-building rule for universal quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	exbidv 1657	Formula-building rule for existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	2albidv 1658	Formula-building rule for 2 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xA.yps <-> A.xA.ych))
Theorem	2exbidv 1659	Formula-building rule for 2 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yps <-> E.xE.ych))
Theorem	3exbidv 1660	Formula-building rule for 3 existential quantifiers (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xE.yE.zps <-> E.xE.yE.zch))
Theorem	4exbidv 1661	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 1662	Special case of Theorem 19.9 of [Margaris] p. 89.
|- (E.xph <-> ph)
Theorem	19.21v 1663	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 1403 via the use of distinct variable conditions combined with ax-17 1317. 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 1777 derived from df-eu 1775. 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 1664	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	19.21aivv 1665	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (ph -> A.xA.yps)
Theorem	19.21adv 1666	Deduction from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	2ax17 1667	Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
|- (ph -> A.xA.yph)
Theorem	alimdv 1668	Deduction from Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))
Theorem	eximdv 1669	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	2alimdv 1670	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xA.yps -> A.xA.ych))
Theorem	2eximdv 1671	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xE.yps -> E.xE.ych))
Theorem	19.23v 1672	Special case of Theorem 19.23 of [Margaris] p. 90.
|- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23vv 1673	Theorem 19.23 of [Margaris] p. 90 extended to two variables.
|- (A.xA.y(ph -> ps) <-> (E.xE.yph -> ps))
Theorem	19.23aiv 1674	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23aivv 1675	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> ps)   =>   |- (E.xE.yph -> ps)
Theorem	19.23advv 1676	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.xE.yps -> ch))
Theorem	19.27v 1677	Theorem 19.27 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28v 1678	Theorem 19.28 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.36v 1679	Special case of Theorem 19.36 of [Margaris] p. 90.
|- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36aiv 1680	Inference from Theorem 19.36 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.12vv 1681	Special case of 19.12 1394 where its converse holds. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (E.xA.y(ph -> ps) <-> A.yE.x(ph -> ps))
Theorem	19.12vvOLD 1682	Special case of 19.12 1394 where its converse holds.
|- (E.xA.y(ph -> ps) <-> A.yE.x(ph -> ps))
Theorem	19.37v 1683	Special case of Theorem 19.37 of [Margaris] p. 90.
|- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.37aiv 1684	Inference from Theorem 19.37 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (ph -> E.xps)
Theorem	19.41v 1685	Special case of Theorem 19.41 of [Margaris] p. 90.
|- (E.x(ph /\ ps) <-> (E.xph /\ ps))
Theorem	19.41vv 1686	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers.
|- (E.xE.y(ph /\ ps) <-> (E.xE.yph /\ ps))
Theorem	19.41vvv 1687	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers.
|- (E.xE.yE.z(ph /\ ps) <-> (E.xE.yE.zph /\ ps))
Theorem	19.42v 1688	Special case of Theorem 19.42 of [Margaris] p. 90.
|- (E.x(ph /\ ps) <-> (ph /\ E.xps))
Theorem	exdistr 1689	Distribution of existential quantifiers.
|- (E.xE.y(ph /\ ps) <-> E.x(ph /\ E.yps))
Theorem	19.42vv 1690	Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers.
|- (E.xE.y(ph /\ ps) <-> (ph /\ E.xE.yps))
Theorem	19.42vvv 1691	Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers.
|- (E.xE.yE.z(ph /\ ps) <-> (ph /\ E.xE.yE.zps))
Theorem	exdistr2 1692	Distribution of existential quantifiers.
|- (E.xE.yE.z(ph /\ ps) <-> E.x(ph /\ E.yE.zps))
Theorem	3exdistr 1693	Distribution of existential quantifiers. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (E.xE.yE.z(ph /\ ps /\ ch) <-> E.x(ph /\ E.y(ps /\ E.zch)))
Theorem	3exdistrOLD 1694	Distribution of existential quantifiers.
|- (E.xE.yE.z(ph /\ ps /\ ch) <-> E.x(ph /\ E.y(ps /\ E.zch)))
Theorem	4exdistr 1695	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 1696	Rule used to change bound variables, using implicit substitition.
|- (x = y -> (ph <-> ps))   =>   |- (A.xph <-> A.yps)
Theorem	cbvexv 1697	Rule used to change bound variables, using implicit substitition.
|- (x = y -> (ph <-> ps))   =>   |- (E.xph <-> E.yps)
Theorem	cbval2 1698	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 1699	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 1700	Rule used to change bound variables, using implicit substitition.
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- (A.xA.yph <-> A.zA.wps)