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-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 - 1001-1100 - Page 11 of 123

Type	Label	Description
Statement
Axiom	ax-9 1001	Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. One thing this axiom tells us is that at least one thing exists (although ax-4 1009 and possibly others also tell us that, i.e. they are not valid in the empty domain of a "free logic.") In this form (not requiring that x and y be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) It is equivalent to axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint); the equivalence is established by ax9o 1158 and ax9 1160. A more convenient form of this axiom is a9e 1161, which has additional remarks. Raph Levien proved the independence of this axiom from the others on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html.
|- -. A.x -. x = y
Axiom	ax-10 1002	Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). The original version of this axiom was ax-10o 1177 ("o" for "old") and was replaced with this shorter ax-10 1002 in May 2008. The old axiom is proved from this one as theorem ax10o 1176. Conversely, this axiom is proved from ax-10o 1177 as theorem ax10 1178.
|- (A.x x = y -> A.y y = x)
Axiom	ax-11 1003	Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent A.x(x = y -> ph) is a way of expressing "y substituted for x in wff ph" (cf. sb6 1305). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. The original version of this axiom was ax-11o 1255 ("o" for "old") and was replaced with this shorter ax-11 1003 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 1254. Conversely, this axiom is proved from ax-11o 1255 as theorem ax11 1256. Juha Arpiainen proved the independence of this axiom (in the form of the older axiom ax-11o 1255) from the others on 19-Jan-2006. See item 9a at http://us.metamath.org/award2003.html. Interestingly, if the wff expression substituted for ph contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-11o 1255 (from which the ax-11 1003 instance follows by theorem ax11 1256.) The proof is by induction on formula length, using ax11eq 1402 and ax11el 1403 for the basis steps and ax11indn 1405, ax11indi 1406, and ax11inda 1410 for the induction steps. See also ax11v 1303 and ax11v2 1252 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.
|- (x = y -> (A.yph -> A.x(x = y -> ph)))
Axiom	ax-12 1004	Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. An open problem is whether this axiom is redundant. Note that the analogous axiom for the membership connective, ax-15 1399, has been shown to be redundant. It is also unknown whether this axiom can be replaced by a shorter formula. However, it can be derived from two slightly shorter formulas, as shown by a12study 1417.
|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
Axiom	ax-13 1005	Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of the e. binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be.
|- (x = y -> (x e. z -> y e. z))
Axiom	ax-14 1006	Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of the e. binary predicate. Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77.
|- (x = y -> (z e. x -> z e. y))
Axiom	ax-17 1007	Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113. This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 999, ax-4 1009 through ax-9 1001, ax-10o 1177, and ax-12 1004 through ax-16 1247: in that system, we can derive any instance of ax-17 1007 not containing wff variables by induction on formula length, using ax17eq 1248 and ax17el 1400 for the basis together hbn 1040, hbal 1041, and hbim 1043. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct).
|- (ph -> A.xph)
Derive ax-4, ax-5o, and ax-6o
Theorem	ax4 1008	Theorem showing that ax-4 1009 can be derived from ax-5 996, ax-gen 999, ax-8 1000, ax-9 1001, ax-11 1003, and ax-17 1007 and is therefore redundant in a system including the latter axioms. Lemma 21 of [Monk2] p. 114. This theorem should not be referenced in any proof. Instead, we will use ax-4 1009 below so that explicit uses of ax-4 1009 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner may wish to accept ax-4 1009 a priori, so that the proof of this theorem (ax4 1008), which involves equality as well as the distinct variable requirements of ax-17 1007, can be put off until those axioms are studied. Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ax-4 1009, ax-5o 1011, ax-6o 1014, ax-9o 1159, ax-10o 1177, ax-11o 1255, ax-15 1399, and ax-16 1247 are proved by theorems ax4 1008, ax5o 1010, ax6o 1013, ax9o 1158, ax10o 1176, ax11o 1254, ax15 1398, and ax16 1246. We never reference those theorems directly - instead, we use the axiom version that immediately follows it - in order to better isolate the uses of the redundant axioms for easier study of subsystems containing them.
|- (A.xph -> ph)
Axiom	ax-4 1009	Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all x, it is true for any specific x (that would typically occur as a free variable in the wff substituted for ph). (A free variable is one that does not occur in the scope of a quantifier: x and y are both free in x = y, but only x is free in A.yx = y.) This is one of the axioms of what we call "pure" predicate calculus (ax-4 1009 through ax-7 998 plus rule ax-gen 999). Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 999. Conditional forms of the converse are given by ax-12 1004, ax-15 1399, ax-16 1247, and ax-17 1007. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1222. An nice alternate axiomatization uses ax467 1059 and ax-5o 1011 in place of ax-4 1009, ax-5 996, ax-6 997, and ax-7 998. This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1008. (We replaced the older ax-5o 1011 and ax-6o 1014 with newer versions ax-5 996 and ax-6 997 in order to prove this redundancy.)
|- (A.xph -> ph)
Theorem	ax5o 1010	Show that the original axiom ax-5o 1011 can be derived from ax-5 996 and others. See ax5 1012 for the rederivation of ax-5 996 from ax-5o 1011. Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114. This theorem should not be referenced in any proof. Instead, use ax-5o 1011 below so that uses of ax-5o 1011 can be more easily identified.
|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
Axiom	ax-5o 1011	Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying ps. Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding ph to "protect" the axiom from a ph containing a free x. One of the 4 axioms of "pure" predicate calculus. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69. This axiom is redundant, as shown by theorem ax5o 1010.
|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
Theorem	ax5 1012	Rederivation of axiom ax-5 996 from the orginal version, ax-5o 1011. See ax5o 1010 for the derivation of ax-5o 1011 from ax-5 996. This theorem should not be referenced in any proof. Instead, use ax-5 996 above so that uses of ax-5 996 can be more easily identified.
|- (A.x(ph -> ps) -> (A.xph -> A.xps))
Theorem	ax6o 1013	Show that the original axiom ax-6o 1014 can be derived from ax-6 997 and others. See ax6 1015 for the rederivation of ax-6 997 from ax-6o 1014. This theorem should not be referenced in any proof. Instead, use ax-6o 1014 below so that uses of ax-6o 1014 can be more easily identified.
|- (-. A.x -. A.xph -> ph)
Axiom	ax-6o 1014	Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). An alternate axiomatization could use ax467 1059 in place of ax-4 1009, ax-6o 1014, and ax-7 998. This axiom is redundant, as shown by theorem ax6o 1013.
|- (-. A.x -. A.xph -> ph)
Theorem	ax6 1015	Rederivation of axiom ax-6 997 from the orginal version, ax-6o 1014. See ax6o 1013 for the derivation of ax-6o 1014 from ax-6 997. This theorem should not be referenced in any proof. Instead, use ax-6 997 above so that uses of ax-6 997 can be more easily identified.
|- (-. A.xph -> A.x -. A.xph)
Predicate calculus without distinct variables
"Pure" predicate calculus ax-4, ax-5o, ax-6o, ax-gen
Syntax	wex 1016	Extend wff definition to include the existential quantifier ("there exists").
wff E.xph
Definition	df-ex 1017	Define existential quantification. E.xph means "there exists at least one set x such that ph is true." Definition of [Margaris] p. 49.
|- (E.xph <-> -. A.x -. ph)
Theorem	a4i 1018	Inference rule reversing generalization.
|- A.xph   =>   |- ph
Theorem	gen2 1019	Generalization applied twice.
|- ph   =>   |- A.xA.yph
Theorem	a4s 1020	Generalization of antecedent.
|- (ph -> ps)   =>   |- (A.xph -> ps)
Theorem	a4sd 1021	Deduction generalizing antecedent.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> ch))
Theorem	mpg 1022	Modus ponens combined with generalization.
|- (A.xph -> ps)   &   |- ph   =>   |- ps
Theorem	mpgbi 1023	Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
|- (A.xph <-> ps)   &   |- ph   =>   |- ps
Theorem	mpgbir 1024	Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
|- (ph <-> A.xps)   &   |- ps   =>   |- ph
Theorem	a5i 1025	Inference from ax-5o 1011.
|- (A.xph -> ps)   =>   |- (A.xph -> A.xps)
Theorem	a6e 1026	Abbreviated version of ax-6o 1014.
|- (E.xA.xph -> ph)
Theorem	a7s 1027	Swap quantifiers in an antecedent.
|- (A.xA.yph -> ps)   =>   |- (A.yA.xph -> ps)
Theorem	19.20i 1028	Inference quantifying both antecedent and consequent.
|- (ph -> ps)   =>   |- (A.xph -> A.xps)
Theorem	19.20i2 1029	Inference doubly quantifying both antecedent and consequent.
|- (ph -> ps)   =>   |- (A.xA.yph -> A.xA.yps)
Theorem	19.20 1030	Theorem 19.20 of [Margaris] p. 90. (The proof was shortened by O'Cat, 30-Mar-2008.)
|- (A.x(ph -> ps) -> (A.xph -> A.xps))
Theorem	19.20ii 1031	Inference quantifying antecedent, nested antecedent, and consequent.
|- (ph -> (ps -> ch))   =>   |- (A.xph -> (A.xps -> A.xch))
Theorem	19.20d 1032	Deduction from Theorem 19.20 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))
Theorem	19.15 1033	Theorem 19.15 of [Margaris] p. 90.
|- (A.x(ph <-> ps) -> (A.xph <-> A.xps))
Theorem	19.21ai 1034	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	albii 1035	Inference adding universal quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.xph <-> A.xps)
Theorem	2albii 1036	Inference adding 2 universal quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.xA.yph <-> A.xA.yps)
Theorem	hbth 1037	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 1038	Closed theorem version of bound-variable hypothesis builder hbn 1040.
|- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))
Theorem	hba1 1039	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 1040	If x is not free in ph, it is not free in -. ph.
|- (ph -> A.xph)   =>   |- (-. ph -> A.x -. ph)
Theorem	hbal 1041	If x is not free in ph, it is not free in A.yph.
|- (ph -> A.xph)   =>   |- (A.yph -> A.xA.yph)
Theorem	hbex 1042	If x is not free in ph, it is not free in E.yph.
|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)
Theorem	hbim 1043	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 1044	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 1045	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 1046	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 1047	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 1048	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 1049	Lemma 24 of [Monk2] p. 114.
|- (A.yA.xph -> A.xA.yA.xph)
Theorem	hbia1 1050	Lemma 23 of [Monk2] p. 114.
|- ((A.xph -> A.xps) -> A.x(A.xph -> A.xps))
Theorem	hbn1 1051	x is not free in -. A.xph.
|- (-. A.xph -> A.x -. A.xph)
Theorem	hbe1 1052	x is not free in E.xph.
|- (E.xph -> A.xE.xph)
Theorem	ax46 1053	Proof of a single axiom that can replace ax-4 1009 and ax-6o 1014. See ax46to4 1054 and ax46to6 1055 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.)
|- ((A.x -. A.xph -> A.xph) -> ph)
Theorem	ax46to4 1054	Re-derivation of ax-4 1009 from ax46 1053. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
|- (A.xph -> ph)
Theorem	ax46to6 1055	Re-derivation of ax-6o 1014 from ax46 1053. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
|- (-. A.x -. A.xph -> ph)
Theorem	ax67 1056	Proof of a single axiom that can replace both ax-6o 1014 and ax-7 998. See ax67to6 1057 and ax67to7 1058 for the re-derivation of those axioms.
|- (-. A.x -. A.yA.xph -> A.yph)
Theorem	ax67to6 1057	Re-derivation of ax-6o 1014 from ax67 1056. Note that ax-6o 1014 and ax-7 998 are not used by the re-derivation.
|- (-. A.x -. A.xph -> ph)
Theorem	ax67to7 1058	Re-derivation of ax-7 998 from ax67 1056. Note that ax-6o 1014 and ax-7 998 are not used by the re-derivation.
|- (A.xA.yph -> A.yA.xph)
Theorem	ax467 1059	Proof of a single axiom that can replace ax-4 1009, ax-6o 1014, and ax-7 998 in a subsystem that includes these axioms plus ax-5o 1011 and ax-gen 999 (and propositional calculus). See ax467to4 1060, ax467to6 1061, and ax467to7 1062 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's ax46 1053.
|- ((A.xA.y -. A.xA.yph -> A.xph) -> ph)
Theorem	ax467to4 1060	Re-derivation of ax-4 1009 from ax467 1059. Only propositional calculus is used by the re-derivation.
|- (A.xph -> ph)
Theorem	ax467to6 1061	Re-derivation of ax-6o 1014 from ax467 1059. Note that ax-6o 1014 and ax-7 998 are not used by the re-derivation. The use of 19.20i 1028 (which uses ax-4 1009) is allowed since we have already proved ax467to4 1060.
|- (-. A.x -. A.xph -> ph)
Theorem	ax467to7 1062	Re-derivation of ax-7 998 from ax467 1059. Note that ax-6o 1014 and ax-7 998 are not used by the re-derivation. The use of 19.20i 1028 (which uses ax-4 1009) is allowed since we have already proved ax467to4 1060.
|- (A.xA.yph -> A.yA.xph)
Theorem	modal-5 1063	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 1064	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 1065	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 1066	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 1067	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 1068	Theorem 19.5 of [Margaris] p. 89.
|- (A.xA.yph <-> A.yA.xph)
Theorem	alnex 1069	Theorem 19.7 of [Margaris] p. 89.
|- (A.x -. ph <-> -. E.xph)
Theorem	alex 1070	Theorem 19.6 of [Margaris] p. 89.
|- (A.xph <-> -. E.x -. ph)
Theorem	19.9t 1071	A closed version of one direction of 19.9 1072.
|- (A.x(ph -> A.xph) -> (E.xph -> ph))
Theorem	19.9 1072	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 1073	A deduction version of one direction of 19.9 1072.
|- (ps -> A.xps)   &   |- (ps -> (ph -> A.xph))   =>   |- (ps -> (E.xph -> ph))
Theorem	exnal 1074	Theorem 19.14 of [Margaris] p. 90.
|- (E.x -. ph <-> -. A.xph)
Theorem	19.22 1075	Theorem 19.22 of [Margaris] p. 90.
|- (A.x(ph -> ps) -> (E.xph -> E.xps))
Theorem	19.22i 1076	Inference adding existential quantifier to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xph -> E.xps)
Theorem	19.22i2 1077	Inference adding 2 existential quantifiers to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xE.yph -> E.xE.yps)
Theorem	alinexa 1078	A transformation of quantifiers and logical connectives.
|- (A.x(ph -> -. ps) <-> -. E.x(ph /\ ps))
Theorem	exanali 1079	A transformation of quantifiers and logical connectives.
|- (E.x(ph /\ -. ps) <-> -. A.x(ph -> ps))
Theorem	alexn 1080	A relationship between two quantifiers and negation.
|- (A.xE.y -. ph <-> -. E.xA.yph)
Theorem	excomim 1081	One direction of Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph -> E.yE.xph)
Theorem	excom 1082	Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph <-> E.yE.xph)
Theorem	19.12 1083	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 1340 and r19.12sn 2505.
|- (E.xA.yph -> A.yE.xph)
Theorem	19.16 1084	Theorem 19.16 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> A.xps))
Theorem	19.17 1085	Theorem 19.17 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph <-> ps) -> (A.xph <-> ps))
Theorem	19.18 1086	Theorem 19.18 of [Margaris] p. 90.
|- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
Theorem	exbii 1087	Inference adding existential quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xph <-> E.xps)
Theorem	2exbii 1088	Inference adding 2 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yph <-> E.xE.yps)
Theorem	3exbii 1089	Inference adding 3 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yE.zph <-> E.xE.yE.zps)
Theorem	exancom 1090	Commutation of conjunction inside an existential quantifier.
|- (E.x(ph /\ ps) <-> E.x(ps /\ ph))
Theorem	19.19 1091	Theorem 19.19 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> E.xps))
Theorem	19.21 1092	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 1093	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 1094	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 1206. 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 1095	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 1096	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xps)   =>   |- (ph -> ps)
Theorem	19.21bbi 1097	Inference removing double quantifier.
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)
Theorem	19.22d 1098	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	19.23 1099	Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23ai 1100	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)