mmtheorems15 - 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 - 1401-1500 - Page 15 of 175

Type	Label	Description
Statement
Theorem	exancom 1401	Commutation of conjunction inside an existential quantifier.
|- (E.x(ph /\ ps) <-> E.x(ps /\ ph))
Theorem	19.19 1402	Theorem 19.19 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> E.xps))
Theorem	19.21 1403	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 1404	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 1405	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 hbequid2 1533. 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 1406	Deduction from Theorem 19.21 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	19.21adOLD 1407	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 1408	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xps)   =>   |- (ph -> ps)
Theorem	19.21bbi 1409	Inference removing double quantifier.
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)
Theorem	eximd 1410	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	19.23 1411	Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23ai 1412	Inference from Theorem 19.23 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23aiOLD 1413	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23bi 1414	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (E.xph -> ps)   =>   |- (ph -> ps)
Theorem	19.23ad 1415	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 1416	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 1417	Theorem 19.26 of [Margaris] p. 90 with two quantifiers.
|- (A.xA.y(ph /\ ps) <-> (A.xA.yph /\ A.xA.yps))
Theorem	19.26-3an 1418	Theorem 19.26 of [Margaris] p. 90 with triple conjunction.
|- (A.x(ph /\ ps /\ ch) <-> (A.xph /\ A.xps /\ A.xch))
Theorem	19.27 1419	Theorem 19.27 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28 1420	Theorem 19.28 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.29 1421	Theorem 19.29 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)
|- ((A.xph /\ E.xps) -> E.x(ph /\ ps))
Theorem	19.29OLD 1422	Theorem 19.29 of [Margaris] p. 90.
|- ((A.xph /\ E.xps) -> E.x(ph /\ ps))
Theorem	19.29r 1423	Variation of Theorem 19.29 of [Margaris] p. 90.
|- ((E.xph /\ A.xps) -> E.x(ph /\ ps))
Theorem	19.29r2 1424	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 1425	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 1426	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 1427	Inference from Theorem 19.35 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (A.xph -> E.xps)
Theorem	19.35ri 1428	Inference from Theorem 19.35 of [Margaris] p. 90.
|- (A.xph -> E.xps)   =>   |- E.x(ph -> ps)
Theorem	19.36 1429	Theorem 19.36 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36i 1430	Inference from Theorem 19.36 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.37 1431	Theorem 19.37 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.38 1432	Theorem 19.38 of [Margaris] p. 90.
|- ((E.xph -> A.xps) -> A.x(ph -> ps))
Theorem	19.39 1433	Theorem 19.39 of [Margaris] p. 90.
|- ((E.xph -> E.xps) -> E.x(ph -> ps))
Theorem	19.24 1434	Theorem 19.24 of [Margaris] p. 90.
|- ((A.xph -> A.xps) -> E.x(ph -> ps))
Theorem	19.25 1435	Theorem 19.25 of [Margaris] p. 90.
|- (A.yE.x(ph -> ps) -> (E.yA.xph -> E.yE.xps))
Theorem	19.30 1436	Theorem 19.30 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (A.x(ph \/ ps) -> (A.xph \/ E.xps))
Theorem	19.30OLD 1437	Theorem 19.30 of [Margaris] p. 90.
|- (A.x(ph \/ ps) -> (A.xph \/ E.xps))
Theorem	19.32 1438	Theorem 19.32 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph \/ ps) <-> (ph \/ A.xps))
Theorem	19.31 1439	Theorem 19.31 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph \/ ps) <-> (A.xph \/ ps))
Theorem	19.43 1440	Theorem 19.43 of [Margaris] p. 90.
|- (E.x(ph \/ ps) <-> (E.xph \/ E.xps))
Theorem	19.44 1441	Theorem 19.44 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph \/ ps) <-> (E.xph \/ ps))
Theorem	19.45 1442	Theorem 19.45 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph \/ ps) <-> (ph \/ E.xps))
Theorem	19.33 1443	Theorem 19.33 of [Margaris] p. 90.
|- ((A.xph \/ A.xps) -> A.x(ph \/ ps))
Theorem	19.33b 1444	The antecedent provides a condition implying the converse of 19.33 1443. Compare Theorem 19.33 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))
Theorem	19.33bOLD 1445	The antecedent provides a condition implying the converse of 19.33 1443. Compare Theorem 19.33 of [Margaris] p. 90.
|- (-. (E.xph /\ E.xps) -> (A.x(ph \/ ps) <-> (A.xph \/ A.xps)))
Theorem	19.34 1446	Theorem 19.34 of [Margaris] p. 90.
|- ((A.xph \/ E.xps) -> E.x(ph \/ ps))
Theorem	19.40 1447	Theorem 19.40 of [Margaris] p. 90.
|- (E.x(ph /\ ps) -> (E.xph /\ E.xps))
Theorem	19.41 1448	Theorem 19.41 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (ps -> A.xps)   =>   |- (E.x(ph /\ ps) <-> (E.xph /\ ps))
Theorem	19.41OLD 1449	Theorem 19.41 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph /\ ps) <-> (E.xph /\ ps))
Theorem	19.42 1450	Theorem 19.42 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph /\ ps) <-> (ph /\ E.xps))
Theorem	alrot4 1451	Rotate 4 universal quantifiers twice.
|- (A.xA.yA.zA.wph <-> A.zA.wA.xA.yph)
Theorem	excom13 1452	Swap 1st and 3rd existential quantifiers.
|- (E.xE.yE.zph <-> E.zE.yE.xph)
Theorem	exrot3 1453	Rotate existential quantifiers.
|- (E.xE.yE.zph <-> E.yE.zE.xph)
Theorem	exrot4 1454	Rotate existential quantifiers twice.
|- (E.xE.yE.zE.wph <-> E.zE.wE.xE.yph)
Theorem	nexr 1455	Inference from 19.8a 1376. (Contributed by Jeff Hankins, 26-Jul-2009.)
|- -. E.xph   =>   |- -. ph
Theorem	nex 1456	Generalization rule for negated wff.
|- -. ph   =>   |- -. E.xph
Theorem	nexd 1457	Deduction for generalization rule for negated wff.
|- (ph -> A.xph)   &   |- (ph -> -. ps)   =>   |- (ph -> -. E.xps)
Theorem	hbim1 1458	A closed form of hbim 1354.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	albid 1459	Formula-building rule for universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.xps <-> A.xch))
Theorem	exbid 1460	Formula-building rule for existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.xps <-> E.xch))
Theorem	exsimpl 1461	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (The proof was shortened by Andrew Salmon, 29-Jun-2011.)
|- (E.x(ph /\ ps) -> E.xph)
Theorem	exsimplOLD 1462	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.)
|- (E.x(ph /\ ps) -> E.xph)
Theorem	exan 1463	Place a conjunct in the scope of an existential quantifier. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- (E.xph /\ ps)   =>   |- E.x(ph /\ ps)
Theorem	exanOLD 1464	Place a conjunct in the scope of an existential quantifier.
|- (E.xph /\ ps)   =>   |- E.x(ph /\ ps)
Theorem	albiim 1465	Split a biconditional and distribute quantifier.
|- (A.x(ph <-> ps) <-> (A.x(ph -> ps) /\ A.x(ps -> ph)))
Theorem	2albiim 1466	Split a biconditional and distribute 2 quantifiers.
|- (A.xA.y(ph <-> ps) <-> (A.xA.y(ph -> ps) /\ A.xA.y(ps -> ph)))
Theorem	hbnd 1467	Deduction form of bound-variable hypothesis builder hbn 1351.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (-. ps -> A.x -. ps))
Theorem	hbimd 1468	Deduction form of bound-variable hypothesis builder hbim 1354.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))
Theorem	hband 1469	Deduction form of bound-variable hypothesis builder hban 1356.
|- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps /\ ch) -> A.x(ps /\ ch)))
Theorem	hbbid 1470	Deduction form of bound-variable hypothesis builder hbbi 1357.
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps <-> ch) -> A.x(ps <-> ch)))
Theorem	hbald 1471	Deduction form of bound-variable hypothesis builder hbal 1352.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (A.yps -> A.xA.yps))
Theorem	hbexd 1472	Deduction form of bound-variable hypothesis builder hbex 1353.
|- (ph -> A.yph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (E.yps -> A.xE.yps))
Theorem	19.21t 1473	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 1474	Closed form of Theorem 19.23 of [Margaris] p. 90.
|- (A.x(ps -> A.xps) -> (A.x(ph -> ps) <-> (E.xph -> ps)))
Theorem	exintr 1475	Introduce a conjunct in the scope of an existential quantifier.
|- (A.x(ph -> ps) -> (E.xph -> E.x(ph /\ ps)))
Theorem	exintrbi 1476	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 1477	Rearrange universal quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (A.xA.y(ph /\ ps) <-> (A.xph /\ A.yps))
Theorem	eeor 1478	Rearrange existential quantifiers.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (E.xE.y(ph \/ ps) <-> (E.xph \/ E.yps))
Theorem	qexmid 1479	Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic.
|- E.x(ph -> A.xph)
Equality
Theorem	ax9o 1480	Show that the original axiom ax-9o 1481 can be derived from ax-9 1307 and others. See ax9 1482 for the rederivation of ax-9 1307 from ax-9o 1481. This theorem should not be referenced in any proof. Instead, use ax-9o 1481 below so that uses of ax-9o 1481 can be more easily identified.
|- (A.x(x = y -> A.xph) -> ph)
Axiom	ax-9o 1481	A variant of ax-9 1307. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint). This axiom is redundant, as shown by theorem ax9o 1480.
|- (A.x(x = y -> A.xph) -> ph)
Theorem	ax9 1482	Rederivation of axiom ax-9 1307 from the orginal version, ax-9o 1481. See ax9o 1480 for the derivation of ax-9o 1481 from ax-9 1307. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). This theorem should not be referenced in any proof. Instead, use ax-9 1307 above so that uses of ax-9 1307 can be more easily identified.
|- -. A.x -. x = y
Theorem	a9e 1483	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 1302 through ax-14 1312 and ax-17 1317, all axioms other than ax-9 1307 are believed to be theorems of free logic, although the system without ax-9 1307 is probably not complete in free logic.
|- E.x x = y
Theorem	equid 1484	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 1317; see the proof of equid1 1646. See equidALT 1485 for an alternate proof.
|- x = x
Theorem	equidALT 1485	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. Alternate proof of equid 1484 directly from equality axioms ax-9 1307 and ax-12 1310.
|- x = x
Theorem	stdpc6 1486	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1544.) 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 1487	Commutative law for equality. Lemma 7 of [Tarski] p. 69.
|- (x = y -> y = x)
Theorem	equcom 1488	Commutative law for equality.
|- (x = y <-> y = x)
Theorem	equcoms 1489	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.
|- (x = y -> ph)   =>   |- (y = x -> ph)
Theorem	equtr 1490	A transitive law for equality.
|- (x = y -> (y = z -> x = z))
Theorem	equtrr 1491	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint).
|- (x = y -> (z = x -> z = y))
Theorem	equtr2 1492	A transitive law for equality. (The proof was shortened by Andrew Salmon, 25-May-2011.)
|- ((x = z /\ y = z) -> x = y)
Theorem	equtr2OLD 1493	A transitive law for equality.
|- ((x = z /\ y = z) -> x = y)
Theorem	equequ1 1494	An equivalence law for equality.
|- (x = y -> (x = z <-> y = z))
Theorem	equequ2 1495	An equivalence law for equality.
|- (x = y -> (z = x <-> z = y))
Theorem	elequ1 1496	An identity law for the non-logical predicate.
|- (x = y -> (x e. z <-> y e. z))
Theorem	elequ2 1497	An identity law for the non-logical predicate.
|- (x = y -> (z e. x <-> z e. y))
Theorem	ax11i 1498	Inference that has ax-11 1309 (without A.y) as its conclusion and 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. 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 1499	Show that ax-10o 1500 can be derived from ax-10 1308. An open problem is whether this theorem can be derived from ax-10 1308 and the others when ax-11 1309 is replaced with ax-11o 1588. See theorem ax10 1501 for the rederivation of ax-10 1308 from ax10o 1499. This theorem should not be referenced in any proof. Instead, use ax-10o 1500 below so that uses of ax-10o 1500 can be more easily identified.
|- (A.x x = y -> (A.xph -> A.yph))
Axiom	ax-10o 1500	Axiom ax-10o 1500 ("o" for "old") was the original version of ax-10 1308, before it was discovered (in May 2008) that the shorter ax-10 1308 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 1499.
|- (A.x x = y -> (A.xph -> A.yph))