P. 17 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1601-1700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.29r2 1601	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
|- ( ( E. x E. y ph /\ A. x A. y ps ) -> E. x E. y ( ph /\ ps ) )
Theorem	19.29x 1602	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
|- ( ( E. x A. y ph /\ A. x E. y ps ) -> E. x E. y ( ph /\ ps ) )
Theorem	19.35-1 1603	Forward direction of Theorem 19.35 of [Margaris] p. 90. The converse holds for classical logic but not (for all propositions) in intuitionistic logic (Contributed by Mario Carneiro, 2-Feb-2015.)
|- ( E. x ( ph -> ps ) -> ( A. x ph -> E. x ps ) )
Theorem	19.35i 1604	Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- E. x ( ph -> ps )   =>    |- ( A. x ph -> E. x ps )
Theorem	19.25 1605	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( A. y E. x ( ph -> ps ) -> ( E. y A. x ph -> E. y E. x ps ) )
Theorem	19.30dc 1606	Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- (DECID E. x ps -> ( A. x ( ph \/ ps ) -> ( A. x ph \/ E. x ps ) ) )
Theorem	19.43 1607	Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )
Theorem	19.33b2 1608	The antecedent provides a condition implying the converse of 19.33 1460. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1609 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.)
|- ( ( -. E. x ph \/ -. E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) )
Theorem	19.33bdc 1609	Converse of 19.33 1460 given -. ( E. x ph /\ E. x ps ) and a decidability condition. Compare Theorem 19.33 of [Margaris] p. 90. For a version which does not require a decidability condition, see 19.33b2 1608 (Contributed by Jim Kingdon, 23-Apr-2018.)
|- (DECID E. x ph -> ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) ) )
Theorem	19.40 1610	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
Theorem	19.40-2 1611	Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ph /\ ps ) -> ( E. x E. y ph /\ E. x E. y ps ) )
Theorem	exintrbi 1612	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
|- ( A. x ( ph -> ps ) -> ( E. x ph <-> E. x ( ph /\ ps ) ) )
Theorem	exintr 1613	Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ( ph /\ ps ) ) )
Theorem	alsyl 1614	Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
|- ( ( A. x ( ph -> ps ) /\ A. x ( ps -> ch ) ) -> A. x ( ph -> ch ) )
Theorem	hbex 1615	If x is not free in ph, it is not free in E. y ph. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( ph -> A. x ph )   =>    |- ( E. y ph -> A. x E. y ph )
Theorem	nfex 1616	If x is not free in ph, it is not free in E. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x E. y ph
Theorem	19.2 1617	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.)
|- ( A. x ph -> E. y ph )
Theorem	i19.24 1618	Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1603, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)
|- ( ( A. x ph -> E. x ps ) -> E. x ( ph -> ps ) )   =>    |- ( ( A. x ph -> A. x ps ) -> E. x ( ph -> ps ) )
Theorem	i19.39 1619	Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1603, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)
|- ( ( A. x ph -> E. x ps ) -> E. x ( ph -> ps ) )   =>    |- ( ( E. x ph -> E. x ps ) -> E. x ( ph -> ps ) )
Theorem	19.9ht 1620	A closed version of one direction of 19.9 1623. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )
Theorem	19.9t 1621	A closed version of 19.9 1623. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.)
|- ( F/ x ph -> ( E. x ph <-> ph ) )
Theorem	19.9h 1622	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. x ph )   =>    |- ( E. x ph <-> ph )
Theorem	19.9 1623	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.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- ( E. x ph <-> ph )
Theorem	alexim 1624	One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1598. (Contributed by Jim Kingdon, 2-Jul-2018.)
|- ( A. x ph -> -. E. x -. ph )
Theorem	exnalim 1625	One direction of Theorem 19.14 of [Margaris] p. 90. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
|- ( E. x -. ph -> -. A. x ph )
Theorem	exanaliim 1626	A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
|- ( E. x ( ph /\ -. ps ) -> -. A. x ( ph -> ps ) )
Theorem	alexnim 1627	A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( A. x E. y -. ph -> -. E. x A. y ph )
Theorem	ax6blem 1628	If x is not free in ph, it is not free in -. ph. This theorem doesn't use ax6b 1629 compared to hbnt 1631. (Contributed by GD, 27-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	ax6b 1629	Quantified Negation. Axiom C5-2 of [Monk2] p. 113. (Contributed by GD, 27-Jan-2018.)
|- ( -. A. x ph -> A. x -. A. x ph )
Theorem	hbn1 1630	x is not free in -. A. x ph. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
|- ( -. A. x ph -> A. x -. A. x ph )
Theorem	hbnt 1631	Closed theorem version of bound-variable hypothesis builder hbn 1632. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbn 1632	If x is not free in ph, it is not free in -. ph. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	hbnd 1633	Deduction form of bound-variable hypothesis builder hbn 1632. (Contributed by NM, 3-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( -. ps -> A. x -. ps ) )
Theorem	nfnt 1634	If x is not free in ph, then it is not free in -. ph. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)
|- ( F/ x ph -> F/ x -. ph )
Theorem	nfnd 1635	Deduction associated with nfnt 1634. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	nfn 1636	Inference associated with nfnt 1634. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x -. ph
Theorem	nfdc 1637	If x is not free in ph, it is not free in DECID ph. (Contributed by Jim Kingdon, 11-Mar-2018.)
|- F/ x ph   =>    |- F/ xDECID ph
Theorem	modal-5 1638	The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)
|- ( -. A. x -. ph -> A. x -. A. x -. ph )
Theorem	19.9d 1639	A deduction version of one direction of 19.9 1623. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- ( ps -> F/ x ph )   =>    |- ( ps -> ( E. x ph -> ph ) )
Theorem	19.9hd 1640	A deduction version of one direction of 19.9 1623. This is an older variation of this theorem; new proofs should use 19.9d 1639. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
|- ( ps -> A. x ps )   &    |- ( ps -> ( ph -> A. x ph ) )   =>    |- ( ps -> ( E. x ph -> ph ) )
Theorem	excomim 1641	One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
|- ( E. x E. y ph -> E. y E. x ph )
Theorem	excom 1642	Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
|- ( E. x E. y ph <-> E. y E. x ph )
Theorem	19.12 1643	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! (Contributed by NM, 5-Aug-1993.)
|- ( E. x A. y ph -> A. y E. x ph )
Theorem	19.19 1644	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( A. x ( ph <-> ps ) -> ( ph <-> E. x ps ) )
Theorem	19.21-2 1645	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
|- F/ x ph   &    |- F/ y ph   =>    |- ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps ) )
Theorem	nf2 1646	An alternate definition of df-nf 1437, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> ( E. x ph -> A. x ph ) )
Theorem	nf3 1647	An alternate definition of df-nf 1437. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> A. x ( E. x ph -> ph ) )
Theorem	nf4dc 1648	Variable x is effectively not free in ph iff ph is always true or always false, given a decidability condition. The reverse direction, nf4r 1649, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- (DECID E. x ph -> ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) ) )
Theorem	nf4r 1649	If ph is always true or always false, then variable x is effectively not free in ph. The converse holds given a decidability condition, as seen at nf4dc 1648. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( ( A. x ph \/ A. x -. ph ) -> F/ x ph )
Theorem	19.36i 1650	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- F/ x ps   &    |- E. x ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	19.36-1 1651	Closed form of 19.36i 1650. One direction of Theorem 19.36 of [Margaris] p. 90. The converse holds in classical logic, but does not hold (for all propositions) in intuitionistic logic. (Contributed by Jim Kingdon, 20-Jun-2018.)
|- F/ x ps   =>    |- ( E. x ( ph -> ps ) -> ( A. x ph -> ps ) )
Theorem	19.37-1 1652	One direction of Theorem 19.37 of [Margaris] p. 90. The converse holds in classical logic but not, in general, here. (Contributed by Jim Kingdon, 21-Jun-2018.)
|- F/ x ph   =>    |- ( E. x ( ph -> ps ) -> ( ph -> E. x ps ) )
Theorem	19.37aiv 1653*	Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- E. x ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.38 1654	Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
Theorem	19.23t 1655	Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- ( F/ x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	19.23 1656	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.32dc 1657	Theorem 19.32 of [Margaris] p. 90, where ph is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
|- F/ x ph   =>    |- (DECID ph -> ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) ) )
Theorem	19.32r 1658	One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if ph is decidable, as seen at 19.32dc 1657. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- F/ x ph   =>    |- ( ( ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
Theorem	19.31r 1659	One direction of Theorem 19.31 of [Margaris] p. 90. The converse holds in classical logic, but not intuitionistic logic. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- F/ x ps   =>    |- ( ( A. x ph \/ ps ) -> A. x ( ph \/ ps ) )
Theorem	19.44 1660	Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ps   =>    |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) )
Theorem	19.45 1661	Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )
Theorem	19.34 1662	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ( A. x ph \/ E. x ps ) -> E. x ( ph \/ ps ) )
Theorem	19.41h 1663	Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1664 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)
|- ( ps -> A. x ps )   =>    |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.41 1664	Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
|- F/ x ps   =>    |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.42h 1665	Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1666 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	19.42 1666	Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- F/ x ph   =>    |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	excom13 1667	Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y E. z ph <-> E. z E. y E. x ph )
Theorem	exrot3 1668	Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)
|- ( E. x E. y E. z ph <-> E. y E. z E. x ph )
Theorem	exrot4 1669	Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y E. z E. w ph <-> E. z E. w E. x E. y ph )
Theorem	nexr 1670	Inference from 19.8a 1569. (Contributed by Jeff Hankins, 26-Jul-2009.)
|- -. E. x ph   =>    |- -. ph
Theorem	exan 1671	Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( E. x ph /\ ps )   =>    |- E. x ( ph /\ ps )
Theorem	hbexd 1672	Deduction form of bound-variable hypothesis builder hbex 1615. (Contributed by NM, 2-Jan-2002.)
|- ( ph -> A. y ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( E. y ps -> A. x E. y ps ) )
Theorem	eeor 1673	Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x E. y ( ph \/ ps ) <-> ( E. x ph \/ E. y ps ) )
1.3.8  Equality theorems without distinct variables
Theorem	a9e 1674	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 1423 through ax-14 1492 and ax-17 1506, all axioms other than ax-9 1511 are believed to be theorems of free logic, although the system without ax-9 1511 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
|- E. x x = y
Theorem	a9ev 1675*	At least one individual exists. Weaker version of a9e 1674. (Contributed by NM, 3-Aug-2017.)
|- E. x x = y
Theorem	ax9o 1676	An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Theorem	equid 1677	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. This proof is similar to Tarski's and makes use of a dummy variable y. It also works in intuitionistic logic, unlike some other possible ways of proving this theorem. (Contributed by NM, 1-Apr-2005.)
|- x = x
Theorem	nfequid 1678	Bound-variable hypothesis builder for x = x. This theorem tells us that any variable, including x, is effectively not free in x = x, even though x is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.)
|- F/ y x = x
Theorem	stdpc6 1679	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1743.) 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). (Contributed by NM, 16-Feb-2005.)
|- A. x x = x
Theorem	equcomi 1680	Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> y = x )
Theorem	ax6evr 1681*	A commuted form of a9ev 1675. The naming reflects how axioms were numbered in the Metamath Proof Explorer as of 2020 (a numbering which we eventually plan to adopt here too, but until this happens everywhere only some theorems will have it). (Contributed by BJ, 7-Dec-2020.)
|- E. x y = x
Theorem	equcom 1682	Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
|- ( x = y <-> y = x )
Theorem	equcomd 1683	Deduction form of equcom 1682, symmetry of equality. For the versions for classes, see eqcom 2141 and eqcomd 2145. (Contributed by BJ, 6-Oct-2019.)
|- ( ph -> x = y )   =>    |- ( ph -> y = x )
Theorem	equcoms 1684	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ph )   =>    |- ( y = x -> ph )
Theorem	equtr 1685	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
|- ( x = y -> ( y = z -> x = z ) )
Theorem	equtrr 1686	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
|- ( x = y -> ( z = x -> z = y ) )
Theorem	equtr2 1687	A transitive law for equality. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ( x = z /\ y = z ) -> x = y )
Theorem	equequ1 1688	An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( x = z <-> y = z ) )
Theorem	equequ2 1689	An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( z = x <-> z = y ) )
Theorem	elequ1 1690	An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( x e. z <-> y e. z ) )
Theorem	elequ2 1691	An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( z e. x <-> z e. y ) )
Theorem	ax11i 1692	Inference that has ax-11 1484 (without A. y) as its conclusion and doesn't require ax-10 1483, ax-11 1484, or ax-12 1489 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. (Contributed by NM, 20-May-2008.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( ps -> A. x ps )   =>    |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
1.3.9  Axioms ax-10 and ax-11
Theorem	ax10o 1693	Show that ax-10o 1694 can be derived from ax-10 1483. An open problem is whether this theorem can be derived from ax-10 1483 and the others when ax-11 1484 is replaced with ax-11o 1795. See theorem ax10 1695 for the rederivation of ax-10 1483 from ax10o 1693. Normally, ax10o 1693 should be used rather than ax-10o 1694, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Axiom	ax-10o 1694	Axiom ax-10o 1694 ("o" for "old") was the original version of ax-10 1483, before it was discovered (in May 2008) that the shorter ax-10 1483 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 1693. Normally, ax10o 1693 should be used rather than ax-10o 1694, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	ax10 1695	Rederivation of ax-10 1483 from original version ax-10o 1694. See theorem ax10o 1693 for the derivation of ax-10o 1694 from ax-10 1483. This theorem should not be referenced in any proof. Instead, use ax-10 1483 above so that uses of ax-10 1483 can be more easily identified. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	hbae 1696	All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
|- ( A. x x = y -> A. z A. x x = y )
Theorem	nfae 1697	All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ z A. x x = y
Theorem	hbaes 1698	Rule that applies hbae 1696 to antecedent. (Contributed by NM, 5-Aug-1993.)
|- ( A. z A. x x = y -> ph )   =>    |- ( A. x x = y -> ph )
Theorem	hbnae 1699	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 5-Aug-1993.)
|- ( -. A. x x = y -> A. z -. A. x x = y )
Theorem	nfnae 1700	All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ z -. A. x x = y