mmtheorems12 - 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 - 1101-1200 - Page 12 of 123

Type	Label	Description
Statement
Theorem	19.23bi 1101	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (E.xph -> ps)   =>   |- (ph -> ps)
Theorem	19.23ad 1102	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	19.26 1103	Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119.
|- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))
Theorem	19.26-2 1104	Theorem 19.26 of [Margaris] p. 90 with two quantifiers.
|- (A.xA.y(ph /\ ps) <-> (A.xA.yph /\ A.xA.yps))
Theorem	19.27 1105	Theorem 19.27 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28 1106	Theorem 19.28 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.29 1107	Theorem 19.29 of [Margaris] p. 90.
|- ((A.xph /\ E.xps) -> E.x(ph /\ ps))
Theorem	19.29r 1108	Variation of Theorem 19.29 of [Margaris] p. 90.
|- ((E.xph /\ A.xps) -> E.x(ph /\ ps))
Theorem	19.29r2 1109	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification.
|- ((E.xE.yph /\ A.xA.yps) -> E.xE.y(ph /\ ps))
Theorem	19.29x 1110	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification.
|- ((E.xA.yph /\ A.xE.yps) -> E.xE.y(ph /\ ps))
Theorem	19.35 1111	Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier.
|- (E.x(ph -> ps) <-> (A.xph -> E.xps))
Theorem	19.35i 1112	Inference from Theorem 19.35 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (A.xph -> E.xps)
Theorem	19.35ri 1113	Inference from Theorem 19.35 of [Margaris] p. 90.
|- (A.xph -> E.xps)   =>   |- E.x(ph -> ps)
Theorem	19.36 1114	Theorem 19.36 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36i 1115	Inference from Theorem 19.36 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.37 1116	Theorem 19.37 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.38 1117	Theorem 19.38 of [Margaris] p. 90.
|- ((E.xph -> A.xps) -> A.x(ph -> ps))
Theorem	19.39 1118	Theorem 19.39 of [Margaris] p. 90.
|- ((E.xph -> E.xps) -> E.x(ph -> ps))
Theorem	19.24 1119	Theorem 19.24 of [Margaris] p. 90.
|- ((A.xph -> A.xps) -> E.x(ph -> ps))
Theorem	19.25 1120	Theorem 19.25 of [Margaris] p. 90.
|- (A.yE.x(ph -> ps) -> (E.yA.xph -> E.yE.xps))
Theorem	19.30 1121	Theorem 19.30 of [Margaris] p. 90.
|- (A.x(ph \/ ps) -> (A.xph \/ E.xps))
Theorem	19.32 1122	Theorem 19.32 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph \/ ps) <-> (ph \/ A.xps))
Theorem	19.31 1123	Theorem 19.31 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph \/ ps) <-> (A.xph \/ ps))
Theorem	19.43 1124	Theorem 19.43 of [Margaris] p. 90.
|- (E.x(ph \/ ps) <-> (E.xph \/ E.xps))
Theorem	19.44 1125	Theorem 19.44 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph \/ ps) <-> (E.xph \/ ps))
Theorem	19.45 1126	Theorem 19.45 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph \/ ps) <-> (ph \/ E.xps))
Theorem	19.33 1127	Theorem 19.33 of [Margaris] p. 90.
|- ((A.xph \/ A.xps) -> A.x(ph \/ ps))
Theorem	19.33b 1128	The antecedent provides a condition implying the converse of 19.33 1127. Compare Theorem 19.33 of [Margaris] p. 90.
|- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))
Theorem	19.34 1129	Theorem 19.34 of [Margaris] p. 90.
|- ((A.xph \/ E.xps) -> E.x(ph \/ ps))
Theorem	19.40 1130	Theorem 19.40 of [Margaris] p. 90.
|- (E.x(ph /\ ps) -> (E.xph /\ E.xps))
Theorem	19.41 1131	Theorem 19.41 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph /\ ps) <-> (E.xph /\ ps))
Theorem	19.42 1132	Theorem 19.42 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph /\ ps) <-> (ph /\ E.xps))
Theorem	alrot4 1133	Rotate 4 universal quantifiers twice.
|- (A.xA.yA.zA.wph <-> A.zA.wA.xA.yph)
Theorem	excom13 1134	Swap 1st and 3rd existential quantifiers.
|- (E.xE.yE.zph <-> E.zE.yE.xph)
Theorem	exrot3 1135	Rotate existential quantifiers.
|- (E.xE.yE.zph <-> E.yE.zE.xph)
Theorem	exrot4 1136	Rotate existential quantifiers twice.
|- (E.xE.yE.zE.wph <-> E.zE.wE.xE.yph)
Theorem	nex 1137	Generalization rule for negated wff.
|- -. ph   =>   |- -. E.xph
Theorem	nexd 1138	Deduction for generalization rule for negated wff.
|- (ph -> A.xph)   &   |- (ph -> -. ps)   =>   |- (ph -> -. E.xps)
Theorem	hbim1 1139	A closed form of hbim 1043.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	albid 1140	Formula-building rule for universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	exbid 1141	Formula-building rule for existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	exan 1142	Place a conjunct in the scope of an existential quantifier.
|- (E.xph /\ ps)   =>   |- E.x(ph /\ ps)
Theorem	albi 1143	Split a biconditional and distribute quantifier.
|- (A.x(ph <-> ps) <-> (A.x(ph -> ps) /\ A.x(ps -> ph)))
Theorem	2albi 1144	Split a biconditional and distribute 2 quantifiers.
|- (A.xA.y(ph <-> ps) <-> (A.xA.y(ph -> ps) /\ A.xA.y(ps -> ph)))
Theorem	hbnd 1145	Deduction form of bound-variable hypothesis builder hbn 1040.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (-. ps -> A.x -. ps))
Theorem	hbimd 1146	Deduction form of bound-variable hypothesis builder hbim 1043.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))
Theorem	hband 1147	Deduction form of bound-variable hypothesis builder hban 1045.
|- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps /\ ch) -> A.x(ps /\ ch)))
Theorem	hbbid 1148	Deduction form of bound-variable hypothesis builder hbbi 1046.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps <-> ch) -> A.x(ps <-> ch)))
Theorem	hbald 1149	Deduction form of bound-variable hypothesis builder hbal 1041.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (A.yps -> A.xA.yps))
Theorem	hbexd 1150	Deduction form of bound-variable hypothesis builder hbex 1042.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (E.yps -> A.xE.yps))
Theorem	19.21t 1151	Closed form of Theorem 19.21 of [Margaris] p. 90.
|- (A.x(ph -> A.xph) -> (A.x(ph -> ps) <-> (ph -> A.xps)))
Theorem	19.23t 1152	Closed form of Theorem 19.23 of [Margaris] p. 90.
|- (A.x(ps -> A.xps) -> (A.x(ph -> ps) <-> (E.xph -> ps)))
Theorem	exintr 1153	Introduce a conjunct in the scope of an existential quantifier.
|- (A.x(ph -> ps) -> (E.xph -> E.x(ph /\ ps)))
Theorem	exintrbi 1154	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
|- (A.x(ph -> ps) -> (E.xph <-> E.x(ph /\ ps)))
Theorem	aaan 1155	Rearrange universal quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (A.xA.y(ph /\ ps) <-> (A.xph /\ A.yps))
Theorem	eeor 1156	Rearrange existential quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (E.xE.y(ph \/ ps) <-> (E.xph \/ E.yps))
Theorem	qexmid 1157	Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic.
|- E.x(ph -> A.xph)
Equality
Theorem	ax9o 1158	Show that the original axiom ax-9o 1159 can be derived from ax-9 1001 and others. See ax9 1160 for the rederivation of ax-9 1001 from ax-9o 1159. This theorem should not be referenced in any proof. Instead, use ax-9o 1159 below so that uses of ax-9o 1159 can be more easily identified.
|- (A.x(x = y -> A.xph) -> ph)
Axiom	ax-9o 1159	A variant of ax-9 1001. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint). This axiom is redundant, as shown by theorem ax9o 1158.
|- (A.x(x = y -> A.xph) -> ph)
Theorem	ax9 1160	Rederivation of axiom ax-9 1001 from the orginal version, ax-9o 1159. See ax9o 1158 for the derivation of ax-9o 1159 from ax-9 1001. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). This theorem should not be referenced in any proof. Instead, use ax-9 1001 above so that uses of ax-9 1001 can be more easily identified.
|- -. A.x -. x = y
Theorem	a9e 1161	At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 996 through ax-14 1006 and ax-17 1007, all axioms other than ax-9 1001 are believed to be theorems of free logic, although the system without ax-9 1001 is probably not complete in free logic.
|- E.x x = y
Theorem	equid 1162	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and thus requires no dummy variables. A simpler proof, similar to Tarki's, is possible if we make use of ax-17 1007; see the proof of equid1 1307. See equidALT 1163 for an alternate proof.
|- x = x
Theorem	equidALT 1163	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. Alternate proof of equid 1162 directly from equality axioms ax-9 1001 and ax-12 1004.
|- x = x
Theorem	stdpc6 1164	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1217.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain).
|- A.x x = x
Theorem	equcomi 1165	Commutative law for equality. Lemma 7 of [Tarski] p. 69.
|- (x = y -> y = x)
Theorem	equcom 1166	Commutative law for equality.
|- (x = y <-> y = x)
Theorem	equcoms 1167	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.
|- (x = y -> ph)   =>   |- (y = x -> ph)
Theorem	equtr 1168	A transitive law for equality.
|- (x = y -> (y = z -> x = z))
Theorem	equtrr 1169	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint).
|- (x = y -> (z = x -> z = y))
Theorem	equtr2 1170	A transitive law for equality.
|- ((x = z /\ y = z) -> x = y)
Theorem	equequ1 1171	An equivalence law for equality.
|- (x = y -> (x = z <-> y = z))
Theorem	equequ2 1172	An equivalence law for equality.
|- (x = y -> (z = x <-> z = y))
Theorem	elequ1 1173	An identity law for the non-logical predicate.
|- (x = y -> (x e. z <-> y e. z))
Theorem	elequ2 1174	An identity law for the non-logical predicate.
|- (x = y -> (z e. x <-> z e. y))
Theorem	ax11i 1175	Inference that has ax-11 1003 (without A.y) as its conclusion and 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. Proof similar to Lemma 16 of [Tarski] p. 70.
|- (x = y -> (ph <-> ps))   &   |- (ps -> A.xps)   =>   |- (x = y -> (ph -> A.x(x = y -> ph)))
Axioms ax-10 and ax-11
Theorem	ax10o 1176	Show that ax-10o 1177 can be derived from ax-10 1002. An open problem is whether this theorem can be derived from ax-10 1002 and the others when ax-11 1003 is replaced with ax-11o 1255. See theorem ax10 1178 for the rederivation of ax-10 1002 from ax10o 1176. This theorem should not be referenced in any proof. Instead, use ax-10o 1177 below so that uses of ax-10o 1177 can be more easily identified.
|- (A.x x = y -> (A.xph -> A.yph))
Axiom	ax-10o 1177	Axiom ax-10o 1177 ("o" for "old") was the original version of ax-10 1002, before it was discovered (in May 2008) that the shorter ax-10 1002 could replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). This axiom is redundant, as shown by theorem ax10o 1176.
|- (A.x x = y -> (A.xph -> A.yph))
Theorem	ax10 1178	Rederivation of ax-10 1002 from original version ax-10o 1177. See theorem ax10o 1176 for the derivation of ax-10o 1177 from ax-10 1002. This theorem should not be referenced in any proof. Instead, use ax-10 1002 above so that uses of ax-10 1002 can be more easily identified.
|- (A.x x = y -> A.y y = x)
Theorem	alequcom 1179	Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).
|- (A.x x = y -> A.y y = x)
Theorem	alequcoms 1180	A commutation rule for identical variable specifiers.
|- (A.x x = y -> ph)   =>   |- (A.y y = x -> ph)
Theorem	nalequcoms 1181	A commutation rule for distinct variable specifiers.
|- (-. A.x x = y -> ph)   =>   |- (-. A.y y = x -> ph)
Theorem	hbae 1182	All variables are effectively bound in an identical variable specifier.
|- (A.x x = y -> A.zA.x x = y)
Theorem	hbaes 1183	Rule that applies hbae 1182 to antecedent.
|- (A.zA.x x = y -> ph)   =>   |- (A.x x = y -> ph)
Theorem	hbnae 1184	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint).
|- (-. A.x x = y -> A.z -. A.x x = y)
Theorem	hbnaes 1185	Rule that applies hbnae 1184 to antecedent.
|- (A.z -. A.x x = y -> ph)   =>   |- (-. A.x x = y -> ph)
Theorem	equs3 1186	Lemma used in proofs of substitution properties.
|- (E.x(x = y /\ ph) <-> -. A.x(x = y -> -. ph))
Theorem	equs4 1187	Lemma used in proofs of substitution properties.
|- (A.x(x = y -> ph) -> E.x(x = y /\ ph))
Theorem	equsal 1188	A useful equivalence related to substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x(x = y -> ph) <-> ps)
Theorem	equsex 1189	A useful equivalence related to substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x(x = y /\ ph) <-> ps)
Theorem	dvelimfALT 1190	Proof of dvelimf 1288 without using ax-11 1003. See dvelimALT 1392 for a proof (of the distinct variable version dvelim 1391) that doesn't require ax-10 1002.
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	dral1 1191	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 -> (ph <-> ps))   =>   |- (A.x x = y -> (A.xph <-> A.yps))
Theorem	dral2 1192	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 -> (ph <-> ps))   =>   |- (A.x x = y -> (A.zph <-> A.zps))
Theorem	drex1 1193	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 -> (ph <-> ps))   =>   |- (A.x x = y -> (E.xph <-> E.yps))
Theorem	drex2 1194	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 -> (ph <-> ps))   =>   |- (A.x x = y -> (E.zph <-> E.zps))
Theorem	a4imt 1195	Closed theorem form of a4im 1196.
|- (A.x((ps -> A.xps) /\ (x = y -> (ph -> ps))) -> (A.xph -> ps))
Theorem	a4im 1196	Specialization, using implicit substitition. Compare Lemma 14 of [Tarski] p. 70. The a4im 1196 series of theorems requires that only one direction of the substitution hypothesis hold.
|- (ps -> A.xps)   &   |- (x = y -> (ph -> ps))   =>   |- (A.xph -> ps)
Theorem	a4ime 1197	Existential introduction, using implicit substitition. Compare Lemma 14 of [Tarski] p. 70.
|- (ph -> A.xph)   &   |- (x = y -> (ph -> ps))   =>   |- (ph -> E.xps)
Theorem	a4imed 1198	Deduction version of a4ime 1197.
|- (ch -> A.xch)   &   |- (ch -> (ph -> A.xph))   &   |- (x = y -> (ph -> ps))   =>   |- (ch -> (ph -> E.xps))
Theorem	cbv1 1199	Rule used to change bound variables, using implicit substitition.
|- (ph -> (ps -> A.yps))   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (x = y -> (ps -> ch)))   =>   |- (A.xA.yph -> (A.xps -> A.ych))
Theorem	cbv2 1200	Rule used to change bound variables, using implicit substitition.
|- (ph -> (ps -> A.yps))   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (x = y -> (ps <-> ch)))   =>   |- (A.xA.yph -> (A.xps <-> A.ych))