P. 19 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1801-1900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exrot3 1801	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 1802	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 )
1.5.3  Axiom scheme ax-12 (Substitution)
Axiom	ax-12 1803	Axiom of 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 2155). 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-c15 2213 and was replaced with this shorter ax-12 1803 in Jan. 2007. The old axiom is proved from this one as theorem axc15 2058. Conversely, this axiom is proved from ax-c15 2213 as theorem ax12 2227. Juha Arpiainen proved the metalogical independence of this axiom (in the form of the older axiom ax-c15 2213) from the others on 19-Jan-2006. See item 9a at http://us.metamath.org/award2003.html. See ax12v 1804 and ax12v2 2056 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions. This axiom scheme is logically redundant (see ax12w 1778) but is used as an auxiliary axiom to achieve metalogical completeness. (Contributed by NM, 22-Jan-2007.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
Theorem	ax12v 1804*	This is a version of ax-12 1803 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See theorem ax12v2 2056 for the rederivation of ax-c15 2213 from this theorem. (Contributed by NM, 5-Aug-1993.) Removed dependencies on ax-10 1786 and ax-13 1968. (Revised by Jim Kingdon, 15-Dec-2017.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
Theorem	ax12vOLD 1805*	Obsolete proof of ax12v 1804 as of 8-Dec-2019. (Contributed by Jim Kingdon, 15-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
Theorem	19.8a 1806	If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1808. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
|- ( ph -> E. x ph )
Theorem	19.8aOLD 1807	Obsolete proof of 19.8a 1806 as of 8-Dec-2019. (Contributed by NM, 9-Jan-1993.) (Revised by Wolf Lammen, 13-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> E. x ph )
Theorem	sp 1808	Specialization. A universally quantified wff implies the wff without a quantifier Axiom scheme B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Also appears as Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). For the axiom of specialization presented in many logic textbooks, see theorem stdpc4 2067. This theorem shows that our obsolete axiom ax-c5 2207 can be derived from the others. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114. It appears that this scheme cannot be derived directly from Tarski's axioms without auxiliary axiom scheme ax-12 1803. It is thought the best we can do using only Tarski's axioms is spw 1756. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
|- ( A. x ph -> ph )
Theorem	axc4 1809	Show that the original axiom ax-c4 2208 can be derived from ax-4 1612 and others. See ax4 2218 for the rederivation of ax-4 1612 from ax-c4 2208. Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114. (Contributed by NM, 21-May-2008.) (Proof modification is discouraged.)
|- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	axc7 1810	Show that the original axiom ax-c7 2209 can be derived from ax-10 1786 and others. See ax10 2219 for the rederivation of ax-10 1786 from ax-c7 2209. Normally, axc7 1810 should be used rather than ax-c7 2209, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.)
|- ( -. A. x -. A. x ph -> ph )
Theorem	axc7e 1811	Abbreviated version of axc7 1810. (Contributed by NM, 5-Aug-1993.)
|- ( E. x A. x ph -> ph )
Theorem	modal-b 1812	The analog in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.)
|- ( ph -> A. x -. A. x -. ph )
Theorem	spi 1813	Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
|- A. x ph   =>    |- ph
Theorem	sps 1814	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
|- ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	2sp 1815	A double specialization (see sp 1808). Another double specialization, closer to PM*11.1, is 2stdpc4 2068. (Contributed by BJ, 15-Sep-2018.)
|- ( A. x A. y ph -> ph )
Theorem	spsd 1816	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> ch ) )
Theorem	19.2g 1817	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. Use 19.2 1723 when sufficient. (Contributed by Mel L. O'Cat, 31-Mar-2008.)
|- ( A. x ph -> E. y ph )
Theorem	19.21bi 1818	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.)
|- ( ph -> A. x ps )   =>    |- ( ph -> ps )
Theorem	19.23bi 1819	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( E. x ph -> ps )   =>    |- ( ph -> ps )
Theorem	nexr 1820	Inference from 19.8a 1806. (Contributed by Jeff Hankins, 26-Jul-2009.)
|- -. E. x ph   =>    |- -. ph
Theorem	nfr 1821	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.)
|- ( F/ x ph -> ( ph -> A. x ph ) )
Theorem	nfri 1822	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- ( ph -> A. x ph )
Theorem	nfrd 1823	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> ( ps -> A. x ps ) )
Theorem	alimd 1824	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	alrimi 1825	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	nfd 1826	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	nfdh 1827	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	alrimdd 1828	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	alrimd 1829	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- F/ x ps   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	eximd 1830	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	nexd 1831	Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> -. ps )   =>    |- ( ph -> -. E. x ps )
Theorem	nexdv 1832*	Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. E. x ps )
Theorem	albid 1833	Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )
Theorem	exbid 1834	Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. x ch ) )
Theorem	nfbidf 1835	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( F/ x ps <-> F/ x ch ) )
Theorem	19.3 1836	A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   =>    |- ( A. x ph <-> ph )
Theorem	19.9ht 1837	A closed version of 19.9 1841. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )
Theorem	19.9t 1838	A closed version of 19.9 1841. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- ( F/ x ph -> ( E. x ph <-> ph ) )
Theorem	19.9h 1839	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.) (Proof shortened by Wolf Lammen, 5-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( E. x ph <-> ph )
Theorem	19.9d 1840	A deduction version of one direction of 19.9 1841. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- ( ps -> F/ x ph )   =>    |- ( ps -> ( E. x ph -> ph ) )
Theorem	19.9 1841	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	hbnt 1842	Closed theorem version of bound-variable hypothesis builder hbn 1843. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbn 1843	If x is not free in ph, it is not free in -. ph. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Dec-2017.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	hba1 1844	x is not free in A. x ph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Dec-2017.)
|- ( A. x ph -> A. x A. x ph )
Theorem	nfa1 1845	x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x A. x ph
Theorem	axc4i 1846	Inference version of axc4 1809. (Contributed by NM, 3-Jan-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	nfnf1 1847	x is not free in F/ x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/ x ph
Theorem	nfnt 1848	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	nfn 1849	Inference associated with nfnt 1848. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x -. ph
Theorem	nfnd 1850	Deduction associated with nfnt 1848. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	nfna1 1851	A convenience theorem particularly designed to remove dependencies on ax-11 1791 in conjunction with disjunctors. (Contributed by Wolf Lammen, 2-Sep-2018.)
|- F/ x -. A. x ph
Theorem	19.21t 1852	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	19.21 1853	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph." (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	19.21h 1854	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph." (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	stdpc5 1855	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis F/ x ph can be thought of as emulating " x is not free in ph." With this definition, 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 nfequid 1741. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
Theorem	19.23t 1856	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 1857	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.23h 1858	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- ( ps -> A. x ps )   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	exlimi 1859	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimih 1860	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- ( ps -> A. x ps )   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimd 1861	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 23-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimdh 1862	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.)
|- ( ph -> A. x ph )   &    |- ( ch -> A. x ch )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	nfdi 1863	Since the converse holds by a1i 11, this inference shows that we can represent a not-free hypothesis with either F/ x ph (inference form) or ( ph -> F/ x ph ) (deduction form). (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.)
|- ( ph -> F/ x ph )   =>    |- F/ x ph
Theorem	nfimd 1864	If in a context x is not free in ps and ch, it is not free in ( ps -> ch ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps -> ch ) )
Theorem	hbim1 1865	A closed form of hbim 1869. (Contributed by NM, 2-Jun-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1 1866	A closed form of nfim 1867. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph -> ps )
Theorem	nfim 1867	If x is not free in ph and ps, it is not free in ( ph -> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -> ps )
Theorem	hbimd 1868	Deduction form of bound-variable hypothesis builder hbim 1869. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
Theorem	hbim 1869	If x is not free in ph and ps, it is not free in ( ph -> ps ). (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	19.27 1870	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 21-Jun-1993.)
|- F/ x ps   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28 1871	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1993.)
|- F/ x ph   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	nfand 1872	If in a context x is not free in ps and ch, it is not free in ( ps /\ ch ). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps /\ ch ) )
Theorem	nf3and 1873	Deduction form of bound-variable hypothesis builder nf3an 1877. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/ x th )   =>    |- ( ph -> F/ x ( ps /\ ch /\ th ) )
Theorem	nfan1 1874	A closed form of nfan 1875. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfan 1875	If x is not free in ph and ps, it is not free in ( ph /\ ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph /\ ps )
Theorem	nfnan 1876	If x is not free in ph and ps, then it is not free in ( ph -/\ ps ). (Contributed by Scott Fenton, 2-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -/\ ps )
Theorem	nf3an 1877	If x is not free in ph, ps, and ch, it is not free in ( ph /\ ps /\ ch ). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph /\ ps /\ ch )
Theorem	hban 1878	If x is not free in ph and ps, it is not free in ( ph /\ ps ). (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
Theorem	hb3an 1879	If x is not free in ph, ps, and ch, it is not free in ( ph /\ ps /\ ch ). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
Theorem	nfbid 1880	If in a context x is not free in ps and ch, it is not free in ( ps <-> ch ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps <-> ch ) )
Theorem	nfbi 1881	If x is not free in ph and ps, it is not free in ( ph <-> ps ). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph <-> ps )
Theorem	nfor 1882	If x is not free in ph and ps, it is not free in ( ph \/ ps ). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph \/ ps )
Theorem	nf3or 1883	If x is not free in ph, ps, and ch, it is not free in ( ph \/ ps \/ ch ). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph \/ ps \/ ch )
Theorem	axc112 1884	Same as axc11 2027 but with reversed antecedent. (Contributed by NM, 25-Jul-2015.)
|- ( A. y y = x -> ( A. x ph -> A. y ph ) )
Theorem	axc11nlem 1885*	Lemma for axc11n 2022. Change bound variable in an equality. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Restructure to ease either bundling, or reducing dependencies on axioms. (Revised by Wolf Lammen, 30-Nov-2019.)
|- ( -. A. y y = x -> ( x = z -> A. y x = z ) )   =>    |- ( A. x x = z -> A. y y = x )
Theorem	aevlem1 1886*	Lemma for aev 1890 and axc16g 1887. Change free and bound variables. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 1968, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.)
|- ( A. z z = w -> A. y y = x )
Theorem	axc16g 1887*	Generalization of axc16 1888. Use the latter when sufficient. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) Remove dependency on ax-13 1968, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	axc16 1888*	Proof of older axiom ax-c16 2216. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	ax16gb 1889*	A generalization of axiom ax-c16 2216. (Contributed by NM, 15-May-1993.)
|- ( A. x x = y -> ( ph <-> A. z ph ) )
Theorem	aev 1890*	A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 1791. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 1968, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.)
|- ( A. x x = y -> A. z w = v )
Theorem	ax16nf 1891*	If dtru 4644 is false, then there is only one element in the universe, so everything satisfies F/. (Contributed by Mario Carneiro, 7-Oct-2016.) Remove dependency on ax-11 1791. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.)
|- ( A. x x = y -> F/ z ph )
Theorem	equsalhw 1892*	Weaker version of equsalh 2010 (requiring distinct variables) without using ax-13 1968. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 28-Dec-2017.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	hbex 1893	If x is not free in ph, it is not free in E. y ph. (Contributed by NM, 12-Mar-1993.)
|- ( ph -> A. x ph )   =>    |- ( E. y ph -> A. x E. y ph )
Theorem	nfal 1894	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x A. y ph
Theorem	nfex 1895	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	nfnf 1896	If x is not free in ph, it is not free in F/ y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x F/ y ph
Theorem	19.12 1897	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 1942 and r19.12sn 4099. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- ( E. x A. y ph -> A. y E. x ph )
Theorem	nfald 1898	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y ps )
Theorem	nfexd 1899	If x is not free in ph, it is not free in E. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E. y ps )
Theorem	nfa2 1900	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x A. y A. x ph