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

Statement List for Metamath Proof Explorer - 1101-1200 - Page 12 of 107

Type	Label	Description
Statement
Theorem	hbim1 1101	A closed form of hbim 1005.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	albid 1102	Formula-building rule for universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	exbid 1103	Formula-building rule for existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	exan 1104	Place a conjunct in the scope of an existential quantifier.
|- (E.xph /\ ps)   =>   |- E.x(ph /\ ps)
Theorem	albi 1105	Split a biconditional and distribute quantifier.
|- (A.x(ph <-> ps) <-> (A.x(ph -> ps) /\ A.x(ps -> ph)))
Theorem	2albi 1106	Split a biconditional and distribute 2 quantifiers.
|- (A.xA.y(ph <-> ps) <-> (A.xA.y(ph -> ps) /\ A.xA.y(ps -> ph)))
Theorem	hbnd 1107	Deduction form of bound-variable hypothesis builder hbn 1002.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (-. ps -> A.x -. ps))
Theorem	hbimd 1108	Deduction form of bound-variable hypothesis builder hbim 1005.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))
Theorem	hband 1109	Deduction form of bound-variable hypothesis builder hban 1007.
|- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps /\ ch) -> A.x(ps /\ ch)))
Theorem	hbbid 1110	Deduction form of bound-variable hypothesis builder hbbi 1008.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps <-> ch) -> A.x(ps <-> ch)))
Theorem	hbald 1111	Deduction form of bound-variable hypothesis builder hbal 1003.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (A.yps -> A.xA.yps))
Theorem	hbexd 1112	Deduction form of bound-variable hypothesis builder hbex 1004.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (E.yps -> A.xE.yps))
Theorem	19.21t 1113	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 1114	Closed form of Theorem 19.23 of [Margaris] p. 90.
|- (A.x(ps -> A.xps) -> (A.x(ph -> ps) <-> (E.xph -> ps)))
Theorem	exintr 1115	Introduce a conjunct in the scope of an existential quantifier.
|- (A.x(ph -> ps) -> (E.xph -> E.x(ph /\ ps)))
Theorem	exintrbi 1116	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 1117	Rearrange universal quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (A.xA.y(ph /\ ps) <-> (A.xph /\ A.yps))
Theorem	eeor 1118	Rearrange existential quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (E.xE.y(ph \/ ps) <-> (E.xph \/ E.yps))
Theorem	qexmid 1119	Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic.
|- E.x(ph -> A.xph)
Equality
Theorem	ax9o 1120	Show that the original axiom ax-9o 1121 can be derived from ax-9 963 and others. See ax9 1122 for the rederivation of ax-9 963 from ax-9o 1121. This theorem should not be referenced in any proof. Instead, use ax-9o 1121 below so that uses of ax-9o 1121 can be more easily identified.
|- (A.x(x = y -> A.xph) -> ph)
Axiom	ax-9o 1121	A variant of ax-9 963. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint). This axiom is redundant, as shown by theorem ax9o 1120.
|- (A.x(x = y -> A.xph) -> ph)
Theorem	ax9 1122	Rederivation of axiom ax-9 963 from the orginal version, ax-9o 1121. See ax9o 1120 for the derivation of ax-9o 1121 from ax-9 963. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). This theorem should not be referenced in any proof. Instead, use ax-9 963 above so that uses of ax-9 963 can be more easily identified.
|- -. A.x -. x = y
Theorem	a9e 1123	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 958 through ax-14 968 and ax-17 969, all axioms other than ax-9 963 are believed to be theorems of free logic, although the system without ax-9 963 is probably not complete in free logic.
|- E.x x = y
Theorem	equid 1124	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 969; see the proof of equid1 1267.
|- x = x
Theorem	stdpc6 1125	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1178.) 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 1126	Commutative law for equality. Lemma 7 of [Tarski] p. 69.
|- (x = y -> y = x)
Theorem	equcom 1127	Commutative law for equality.
|- (x = y <-> y = x)
Theorem	equcoms 1128	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.
|- (x = y -> ph)   =>   |- (y = x -> ph)
Theorem	equtr 1129	A transitive law for equality.
|- (x = y -> (y = z -> x = z))
Theorem	equtrr 1130	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint).
|- (x = y -> (z = x -> z = y))
Theorem	equtr2 1131	A transitive law for equality.
|- ((x = z /\ y = z) -> x = y)
Theorem	equequ1 1132	An equivalence law for equality.
|- (x = y -> (x = z <-> y = z))
Theorem	equequ2 1133	An equivalence law for equality.
|- (x = y -> (z = x <-> z = y))
Theorem	elequ1 1134	An identity law for the non-logical predicate.
|- (x = y -> (x e. z <-> y e. z))
Theorem	elequ2 1135	An identity law for the non-logical predicate.
|- (x = y -> (z e. x <-> z e. y))
Theorem	ax11i 1136	Inference that has ax-11 965 (without A.y) as its conclusion and doesn't require ax-10 964, ax-11 965, or ax-12 966 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 1137	Show that ax-10o 1138 can be derived from ax-10 964. An open problem is whether this theorem can be derived from ax-10 964 and the others when ax-11 965 is replaced with ax-11o 1216. See theorem ax10 1139 for the rederivation of ax-10 964 from ax10o 1137. This theorem should not be referenced in any proof. Instead, use ax-10o 1138 below so that uses of ax-10o 1138 can be more easily identified.
|- (A.x x = y -> (A.xph -> A.yph))
Axiom	ax-10o 1138	Axiom ax-10o 1138 ("o" for "old") was the original version of ax-10 964, before it was discovered (in May 2008) that the shorter ax-10 964 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 1137.
|- (A.x x = y -> (A.xph -> A.yph))
Theorem	ax10 1139	Rederivation of ax-10 964 from original version ax-10o 1138. See theorem ax10o 1137 for the derivation of ax-10o 1138 from ax-10 964. This theorem should not be referenced in any proof. Instead, use ax-10 964 above so that uses of ax-10 964 can be more easily identified.
|- (A.x x = y -> A.y y = x)
Theorem	alequcom 1140	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 1141	A commutation rule for identical variable specifiers.
|- (A.x x = y -> ph)   =>   |- (A.y y = x -> ph)
Theorem	nalequcoms 1142	A commutation rule for distinct variable specifiers.
|- (-. A.x x = y -> ph)   =>   |- (-. A.y y = x -> ph)
Theorem	hbae 1143	All variables are effectively bound in an identical variable specifier.
|- (A.x x = y -> A.zA.x x = y)
Theorem	hbaes 1144	Rule that applies hbae 1143 to antecedent.
|- (A.zA.x x = y -> ph)   =>   |- (A.x x = y -> ph)
Theorem	hbnae 1145	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 1146	Rule that applies hbnae 1145 to antecedent.
|- (A.z -. A.x x = y -> ph)   =>   |- (-. A.x x = y -> ph)
Theorem	equs3 1147	Lemma used in proofs of substitution properties.
|- (E.x(x = y /\ ph) <-> -. A.x(x = y -> -. ph))
Theorem	equs4 1148	Lemma used in proofs of substitution properties.
|- (A.x(x = y -> ph) -> E.x(x = y /\ ph))
Theorem	equsal 1149	A useful equivalence related to substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x(x = y -> ph) <-> ps)
Theorem	equsex 1150	A useful equivalence related to substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x(x = y /\ ph) <-> ps)
Theorem	dvelimfALT 1151	Proof of dvelimf 1248 without using ax-11 965. See dvelimALT 1351 for a proof (of the distinct variable version dvelim 1350) that doesn't require ax-10 964.
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	dral1 1152	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 1153	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 1154	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 1155	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 1156	Closed theorem form of a4im 1157.
|- (A.x((ps -> A.xps) /\ (x = y -> (ph -> ps))) -> (A.xph -> ps))
Theorem	a4im</