mmtheorems11 - 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-10774

Statement List for Metamath Proof Explorer - 1001-1100 - Page 11 of 108

Type	Label	Description
Statement
Theorem	19.21ai 1001	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	albii 1002	Inference adding universal quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.xph <-> A.xps)
Theorem	2albii 1003	Inference adding 2 universal quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.xA.yph <-> A.xA.yps)
Theorem	hbth 1004	No variable is (effectively) free in a theorem. This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form |- (ph -> A.xph) from smaller formulas of this form. These are useful for constructing hypotheses that state "x is (effectively) not free in ph."
|- ph   =>   |- (ph -> A.xph)
Theorem	hbnt 1005	Closed theorem version of bound-variable hypothesis builder hbn 1007.
|- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))
Theorem	hba1 1006	x is not free in A.xph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114.
|- (A.xph -> A.xA.xph)
Theorem	hbn 1007	If x is not free in ph, it is not free in -. ph.
|- (ph -> A.xph)   =>   |- (-. ph -> A.x -. ph)
Theorem	hbal 1008	If x is not free in ph, it is not free in A.yph.
|- (ph -> A.xph)   =>   |- (A.yph -> A.xA.yph)
Theorem	hbex 1009	If x is not free in ph, it is not free in E.yph.
|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)
Theorem	hbim 1010	If x is not free in ph and ps, it is not free in (ph -> ps). (The proof was shortened by O'Cat, 3-Mar-2008.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	hbor 1011	If x is not free in ph and ps, it is not free in (ph \/ ps).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph \/ ps) -> A.x(ph \/ ps))
Theorem	hban 1012	If x is not free in ph and ps, it is not free in (ph /\ ps).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph /\ ps) -> A.x(ph /\ ps))
Theorem	hbbi 1013	If x is not free in ph and ps, it is not free in (ph <-> ps).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph <-> ps) -> A.x(ph <-> ps))
Theorem	hb3or 1014	If x is not free in ph, ps, and ch, it is not free in (ph \/ ps \/ ch).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph \/ ps \/ ch) -> A.x(ph \/ ps \/ ch))
Theorem	hb3an 1015	If x is not free in ph, ps, and ch, it is not free in (ph /\ ps /\ ch).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph /\ ps /\ ch) -> A.x(ph /\ ps /\ ch))
Theorem	hba2 1016	Lemma 24 of [Monk2] p. 114.
|- (A.yA.xph -> A.xA.yA.xph)
Theorem	hbia1 1017	Lemma 23 of [Monk2] p. 114.
|- ((A.xph -> A.xps) -> A.x(A.xph -> A.xps))
Theorem	hbn1 1018	x is not free in -. A.xph.
|- (-. A.xph -> A.x -. A.xph)
Theorem	hbe1 1019	x is not free in E.xph.
|- (E.xph -> A.xE.xph)
Theorem	ax46 1020	Proof of a single axiom that can replace ax-4 976 and ax-6o 981. See ax46to4 1021 and ax46to6 1022 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.)
|- ((A.x -. A.xph -> A.xph) -> ph)
Theorem	ax46to4 1021	Re-derivation of ax-4 976 from ax46 1020. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
|- (A.xph -> ph)
Theorem	ax46to6 1022	Re-derivation of ax-6o 981 from ax46 1020. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
|- (-. A.x -. A.xph -> ph)
Theorem	ax67 1023	Proof of a single axiom that can replace both ax-6o 981 and ax-7 965. See ax67to6 1024 and ax67to7 1025 for the re-derivation of those axioms.
|- (-. A.x -. A.yA.xph -> A.yph)
Theorem	ax67to6 1024	Re-derivation of ax-6o 981 from ax67 1023. Note that ax-6o 981 and ax-7 965 are not used by the re-derivation.
|- (-. A.x -. A.xph -> ph)
Theorem	ax67to7 1025	Re-derivation of ax-7 965 from ax67 1023. Note that ax-6o 981 and ax-7 965 are not used by the re-derivation.
|- (A.xA.yph -> A.yA.xph)
Theorem	ax467 1026	Proof of a single axiom that can replace ax-4 976, ax-6o 981, and ax-7 965 in a subsystem that includes these axioms plus ax-5o 978 and ax-gen 966 (and propositional calculus). See ax467to4 1027, ax467to6 1028, and ax467to7 1029 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's ax46 1020.
|- ((A.xA.y -. A.xA.yph -> A.xph) -> ph)
Theorem	ax467to4 1027	Re-derivation of ax-4 976 from ax467 1026. Only propositional calculus is used by the re-derivation.
|- (A.xph -> ph)
Theorem	ax467to6 1028	Re-derivation of ax-6o 981 from ax467 1026. Note that ax-6o 981 and ax-7 965 are not used by the re-derivation. The use of 19.20i 995 (which uses ax-4 976) is allowed since we have already proved ax467to4 1027.
|- (-. A.x -. A.xph -> ph)
Theorem	ax467to7 1029	Re-derivation of ax-7 965 from ax467 1026. Note that ax-6o 981 and ax-7 965 are not used by the re-derivation. The use of 19.20i 995 (which uses ax-4 976) is allowed since we have already proved ax467to4 1027.
|- (A.xA.yph -> A.yA.xph)
Theorem	modal-5 1030	The analog in our "pure" predicate calculus of axiom 5 of modal logic S5.
|- (-. A.x -. ph -> A.x -. A.x -. ph)
Theorem	modal-b 1031	The analog in our "pure" predicate calculus of the Brouwer axiom (B) of modal logic S5.
|- (ph -> A.x -. A.x -. ph)
Theorem	19.8a 1032	If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89.
|- (ph -> E.xph)
Theorem	19.2 1033	Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.)
|- (A.xph -> E.yph)
Theorem	19.3 1034	A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89.
|- (ph -> A.xph)   =>   |- (A.xph <-> ph)
Theorem	alcom 1035	Theorem 19.5 of [Margaris] p. 89.
|- (A.xA.yph <-> A.yA.xph)
Theorem	alnex 1036	Theorem 19.7 of [Margaris] p. 89.
|- (A.x -. ph <-> -. E.xph)
Theorem	alex 1037	Theorem 19.6 of [Margaris] p. 89.
|- (A.xph <-> -. E.x -. ph)
Theorem	19.9t 1038	A closed version of one direction of 19.9 1039.
|- (A.x(ph -> A.xph) -> (E.xph -> ph))
Theorem	19.9 1039	A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.)
|- (ph -> A.xph)   =>   |- (E.xph <-> ph)
Theorem	19.9d 1040	A deduction version of one direction of 19.9 1039.
|- (ps -> A.xps)   &   |- (ps -> (ph -> A.xph))   =>   |- (ps -> (E.xph -> ph))
Theorem	exnal 1041	Theorem 19.14 of [Margaris] p. 90.
|- (E.x -. ph <-> -. A.xph)
Theorem	19.22 1042	Theorem 19.22 of [Margaris] p. 90.
|- (A.x(ph -> ps) -> (E.xph -> E.xps))
Theorem	19.22i 1043	Inference adding existential quantifier to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xph -> E.xps)
Theorem	19.22i2 1044	Inference adding 2 existential quantifiers to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xE.yph -> E.xE.yps)
Theorem	alinexa 1045	A transformation of quantifiers and logical connectives.
|- (A.x(ph -> -. ps) <-> -. E.x(ph /\ ps))
Theorem	exanali 1046	A transformation of quantifiers and logical connectives.
|- (E.x(ph /\ -. ps) <-> -. A.x(ph -> ps))
Theorem	alexn 1047	A relationship between two quantifiers and negation.
|- (A.xE.y -. ph <-> -. E.xA.yph)
Theorem	excomim 1048	One direction of Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph -> E.yE.xph)
Theorem	excom 1049	Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph <-> E.yE.xph)
Theorem	19.12 1050	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 1305 and r19.12sn 2451.
|- (E.xA.yph -> A.yE.xph)
Theorem	19.16 1051	Theorem 19.16 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> A.xps))
Theorem	19.17 1052	Theorem 19.17 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph <-> ps) -> (A.xph <-> ps))
Theorem	19.18 1053	Theorem 19.18 of [Margaris] p. 90.
|- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
Theorem	exbii 1054	Inference adding existential quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xph <-> E.xps)
Theorem	2exbii 1055	Inference adding 2 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yph <-> E.xE.yps)
Theorem	3exbi 1056	Inference adding 3 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yE.zph <-> E.xE.yE.zps)
Theorem	exancom 1057	Commutation of conjunction inside an existential quantifier.
|- (E.x(ph /\ ps) <-> E.x(ps /\ ph))
Theorem	19.19 1058	Theorem 19.19 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> E.xps))
Theorem	19.21 1059	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in ph."
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	19.21-2 1060	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers.
|- (ph -> A.xph)   &   |- (ph -> A.yph)   =>   |- (A.xA.y(ph -> ps) <-> (ph -> A.xA.yps))
Theorem	stdpc5 1061	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis (ph -> A.xph) can be thought of as emulating "x is not free in ph." With this convention, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by hbequid 1172. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5.
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) -> (ph -> A.xps))
Theorem	19.21ad 1062	Deduction from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	19.21bi 1063	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xps)   =>   |- (ph -> ps)
Theorem	19.21bbi 1064	Inference removing double quantifier.
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)