P. 22 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2101-2200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.32 2101	Theorem 19.32 of [Margaris] p. 90. See 19.32v 1869 for a version requiring fewer axioms. (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.31 2102	Theorem 19.31 of [Margaris] p. 90. See 19.31v 1870 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.)
|- F/ x ps   =>    |- ( A. x ( ph \/ ps ) <-> ( A. x ph \/ ps ) )
Theorem	19.41 2103	Theorem 19.41 of [Margaris] p. 90. See 19.41v 1914 for a version requiring fewer axioms. (Contributed by NM, 14-May-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.42-1 2104	One direction of 19.42 2105. (Contributed by Wolf Lammen, 10-Jul-2021.)
|- F/ x ph   =>    |- ( ( ph /\ E. x ps ) -> E. x ( ph /\ ps ) )
Theorem	19.42 2105	Theorem 19.42 of [Margaris] p. 90. See 19.42v 1918 for a version requiring fewer axioms. See exan 1788 for an immediate version. (Contributed by NM, 18-Aug-1993.)
|- F/ x ph   =>    |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	19.44 2106	Theorem 19.44 of [Margaris] p. 90. See 19.44v 1912 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
|- F/ x ps   =>    |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) )
Theorem	19.45 2107	Theorem 19.45 of [Margaris] p. 90. See 19.45v 1913 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )
Theorem	equsalv 2108*	Version of equsal 2291 with a dv condition, which does not require ax-13 2246. See equsalvw 1931 for a version with two dv conditions requiring fewer axioms. See also the dual form equsexv 2109. (Contributed by BJ, 31-May-2019.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	equsexv 2109*	Version of equsex 2292 with a dv condition, which does not require ax-13 2246. See equsexvw 1932 for a version with two dv conditions requiring fewer axioms. See also the dual form equsalv 2108. (Contributed by BJ, 31-May-2019.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	sbequ1 2110	An equality theorem for substitution. (Contributed by NM, 16-May-1993.)
|- ( x = y -> ( ph -> [ y / x ] ph ) )
Theorem	sbequ12 2111	An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
|- ( x = y -> ( ph <-> [ y / x ] ph ) )
Theorem	sbequ12r 2112	An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
|- ( x = y -> ( [ x / y ] ph <-> ph ) )
Theorem	sbequ12a 2113	An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.)
|- ( x = y -> ( [ y / x ] ph <-> [ x / y ] ph ) )
Theorem	sbid 2114	An identity theorem for substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
|- ( [ x / x ] ph <-> ph )
Theorem	spimv1 2115*	Version of spim 2254 with a dv condition, which does not require ax-13 2246. See spimvw 1927 for a version with two dv conditions, requiring fewer axioms, and spimv 2257 for another variant. (Contributed by BJ, 31-May-2019.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	nf5 2116	Alternate definition of df-nf 1710. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1710 changed. (Revised by Wolf Lammen, 11-Sep-2021.)
|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
Theorem	nf6 2117	An alternate definition of df-nf 1710. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> A. x ( E. x ph -> ph ) )
Theorem	nf5d 2118	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	nf5di 2119	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	19.9h 2120	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.) (Proof shortened by Wolf Lammen, 14-Jul-2020.)
|- ( ph -> A. x ph )   =>    |- ( E. x ph <-> ph )
Theorem	19.21h 2121	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph." See also 19.21 2075 and 19.21v 1868. (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	19.23h 2122	Theorem 19.23 of [Margaris] p. 90. See 19.23 2080. (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	equsalhw 2123*	Weaker version of equsalh 2294 with a dv condition which does not require ax-13 2246. (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	equsexhv 2124*	Version of equsexh 2295 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	hbim1 2125	A closed form of hbim 2127. (Contributed by NM, 2-Jun-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	hbimd 2126	Deduction form of bound-variable hypothesis builder hbim 2127. (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 2127	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	hban 2128	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 2129	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	axc4 2130	Show that the original axiom ax-c4 34169 can be derived from ax-4 1737 (alim 1738), ax-10 2019 (hbn1 2020), sp 2053 and propositional calculus. See ax4fromc4 34179 for the rederivation of ax-4 1737 from ax-c4 34169. 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	axc4i 2131	Inference version of axc4 2130. (Contributed by NM, 3-Jan-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	axc7 2132	Show that the original axiom ax-c7 34170 can be derived from ax-10 2019 (hbn1 2020) , sp 2053 and propositional calculus. See ax10fromc7 34180 for the rederivation of ax-10 2019 from ax-c7 34170. Normally, axc7 2132 should be used rather than ax-c7 34170, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.)
|- ( -. A. x -. A. x ph -> ph )
Theorem	axc7e 2133	Abbreviated version of axc7 2132 using the existential quantifier. (Contributed by NM, 5-Aug-1993.)
|- ( E. x A. x ph -> ph )
Theorem	axc16g 2134*	Generalization of axc16 2135. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 1935 }, theorem ax12v 2048. (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 2246, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2139. (Revised by Wolf Lammen, 11-Oct-2021.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	axc16 2135*	Proof of older axiom ax-c16 34177. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	axc16gb 2136*	Biconditional strengthening of axc16g 2134. (Contributed by NM, 15-May-1993.)
|- ( A. x x = y -> ( ph <-> A. z ph ) )
Theorem	axc16nf 2137*	If dtru 4857 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 2034. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2019. (Revised by Wolf lammen, 12-Oct-2021.)
|- ( A. x x = y -> F/ z ph )
Theorem	axc11v 2138*	Version of axc11 2314 with a disjoint variable condition on x and y, which is provable, on top of { ax-1 6-- ax-7 1935 }, from ax12v 2048 (contrary to axc11 2314 which seems to require the full ax-12 2047 and ax-13 2246). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	axc11rv 2139*	Version of axc11r 2187 with a disjoint variable condition on x and y, which is provable, on top of { ax-1 6-- ax-7 1935 }, from ax12v 2048 (contrary to axc11 2314 which seems to require the full ax-12 2047). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
|- ( A. x x = y -> ( A. y ph -> A. x ph ) )
Theorem	axc11rvOLD 2140*	Obsolete proof of axc11rv 2139 as of 11-Oct-2021. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( A. y ph -> A. x ph ) )
Theorem	axc11vOLD 2141*	Obsolete proof of axc11v 2138 as of 11-Oct-2021. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	modal-b 2142	The analogue 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	19.9ht 2143	A closed version of 19.9 2072. (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	hbnt 2144	Closed theorem version of bound-variable hypothesis builder hbn 2146. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) (Proof shortened by Wolf Lammen, 14-Oct-2021.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbntOLD 2145	Obsolete proof of hbnt 2144 as of 13-Oct-2021. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbn 2146	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	hbnd 2147	Deduction form of bound-variable hypothesis builder hbn 2146. (Contributed by NM, 3-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( -. ps -> A. x -. ps ) )
Theorem	exlimih 2148	Inference associated with 19.23 2080. See exlimiv 1858 for a version with a dv condition requiring fewer axioms. (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	exlimdh 2149	Deduction form of 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	sb56 2150*	Two equivalent ways of expressing the proper substitution of y for x in ph, when x and y are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1881. The implication "to the left" is equs4 2290 and does not require any dv condition (but the version with a dv condition, equs4v 1930, requires fewer axioms). Theorem equs45f 2350 replaces the dv condition with a non-freeness hypothesis and equs5 2351 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2109 in place of equsex 2292 in order to remove dependency on ax-13 2246. (Revised by BJ, 20-Dec-2020.)
|- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
Theorem	hba1 2151	The setvar x is not free in A. x ph. This corresponds to the axiom (4) of modal logic. 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.) (Proof shortened by Wolf Lammen, 12-Oct-2021.)
|- ( A. x ph -> A. x A. x ph )
Theorem	hbexOLD 2152	Obsolete proof of hbex 2156 as of 16-Oct-2021. (Contributed by NM, 12-Mar-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( E. y ph -> A. x E. y ph )
Theorem	nfal 2153	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 2154	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.) Reduce symbol count in nfex 2154, hbex 2156. (Revised by Wolf Lammen, 16-Oct-2021.)
|- F/ x ph   =>    |- F/ x E. y ph
Theorem	nfexOLD 2155	Obsolete proof of nfex 2154 as of 16-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- F/ x E. y ph
Theorem	hbex 2156	If x is not free in ph, it is not free in E. y ph. (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex 2154, hbex 2156. (Revised by Wolf Lammen, 16-Oct-2021.)
|- ( ph -> A. x ph )   =>    |- ( E. y ph -> A. x E. y ph )
Theorem	nfa1OLD 2157	Obsolete proof of nfa1 2028 as of 12-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1710 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x A. x ph
Theorem	nfnf 2158	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	nfnf1OLD 2159	Obsolete proof of nfnf1 2031 as of 12-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x F/ x ph
Theorem	axc11nlemOLD 2160*	Obsolete proof of axc11nlemOLD2 1988 as of 14-Mar-2021. (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.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( -. A. y y = x -> ( x = z -> A. y x = z ) )   =>    |- ( A. x x = z -> A. y y = x )
Theorem	axc16gOLD 2161*	Obsolete proof of axc16g 2134 as of 11-Oct-2021. (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 2246, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2139. (Revised by Wolf Lammen, 11-Oct-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	aevOLD 2162*	Obsolete proof of aev 1983 as of 19-Mar-2021. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2246, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x x = y -> A. z w = v )
Theorem	axc16nfOLD 2163*	Obsolete proof of axc16nf 2137 as of 12-Oct-2021. (Contributed by Mario Carneiro, 7-Oct-2016.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x x = y -> F/ z ph )
Theorem	19.12 2164	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 2180 and r19.12sn 4255. (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 2165	Deduction form of nfal 2153. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.) (Proof shortened by Wolf Lammen, 16-Oct-2021.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y ps )
Theorem	nfaldOLD 2166	Obsolete proof of nfald 2165 as of 16-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y ps )
Theorem	nfexd 2167	If x is not free in ps, it is not free in E. y ps. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E. y ps )
Theorem	nfa2OLD 2168	Obsolete proof of nfa2 2040 as of 18-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x A. y A. x ph
Theorem	exanOLDOLD 2169	Obsolete proof of exan 1788 as of 7-Jul-2021. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. x ph /\ ps )   =>    |- E. x ( ph /\ ps )
Theorem	aaan 2170	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( A. x A. y ( ph /\ ps ) <-> ( A. x ph /\ A. y ps ) )
Theorem	eeor 2171	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 ) )
Theorem	cbv3v 2172*	Version of cbv3 2265 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	dvelimhw 2173*	Proof of dvelimh 2336 without using ax-13 2246 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 23-Dec-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   &    |- ( -. A. x x = y -> ( y = z -> A. x y = z ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	cbv3hv 2174*	Version of cbv3h 2266 with a dv condition on x , y, which does not require ax-13 2246. Was used in a proof of axc11n 2307 (but of independent interest). (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 29-Nov-2020.) (Proof shortened by BJ, 30-Nov-2020.)
|- ( ph -> A. y ph )   &    |- ( ps -> A. x ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	cbvalv1 2175*	Version of cbval 2271 with a dv condition, which does not require ax-13 2246. See cbvalvw 1969 for a version with two dv conditions, requiring fewer axioms, and cbvalv 2273 for another variant. (Contributed by BJ, 31-May-2019.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvexv1 2176*	Version of cbvex 2272 with a dv condition, which does not require ax-13 2246. See cbvexvw 1970 for a version with two dv conditions, requiring fewer axioms, and cbvexv 2275 for another variant. (Contributed by BJ, 31-May-2019.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	equs5aALT 2177	Alternate proof of equs5a 2348. Uses ax-12 2047 but not ax-13 2246. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. x ( x = y /\ A. y ph ) -> A. x ( x = y -> ph ) )
Theorem	equs5eALT 2178	Alternate proof of equs5e 2349. Uses ax-12 2047 but not ax-13 2246. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. x ( x = y /\ ph ) -> A. x ( x = y -> E. y ph ) )
Theorem	pm11.53 2179*	Theorem *11.53 in [WhiteheadRussell] p. 164. See pm11.53v 1906 for a version requiring fewer axioms. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph -> ps ) <-> ( E. x ph -> A. y ps ) )
Theorem	19.12vv 2180*	Special case of 19.12 2164 where its converse holds. See 19.12vvv 1907 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 18-Jul-2001.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )
Theorem	eean 2181	Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	eeanv 2182*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	eeeanv 2183*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) Reduce distinct variable restrictions. (Revised by Wolf Lammen, 20-Jan-2018.)
|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> ( E. x ph /\ E. y ps /\ E. z ch ) )
Theorem	ee4anv 2184*	Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
|- ( E. x E. y E. z E. w ( ph /\ ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )
Theorem	cleljustALT 2185*	Alternate proof of cleljust 1998. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how DV conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x e. y <-> E. z ( z = x /\ z e. y ) )
Theorem	cleljustALT2 2186*	Alternate proof of cleljust 1998. Compared with cleljustALT 2185, it uses nfv 1843 followed by equsexv 2109 instead of ax-5 1839 followed by equsexhv 2124, so it uses the idiom F/ x ph instead of ph -> A. x ph to express non-freeness. This style is generally preferred for later theorems. (Contributed by NM, 28-Jan-2004.) (Revised by Mario Carneiro, 21-Dec-2016.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x e. y <-> E. z ( z = x /\ z e. y ) )
Theorem	axc11r 2187	Same as axc11 2314 but with reversed antecedent. Note the use of ax-12 2047 (and not merely ax12v 2048). (Contributed by NM, 25-Jul-2015.)
|- ( A. y y = x -> ( A. x ph -> A. y ph ) )
Theorem	nfrOLD 2188	Obsolete proof of nf5r 2064 as of 6-Oct-2021. (Contributed by Mario Carneiro, 26-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( F/ x ph -> ( ph -> A. x ph ) )
Theorem	nfriOLD 2189	Obsolete proof of nf5ri 2065 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- ( ph -> A. x ph )
Theorem	nfrdOLD 2190	Obsolete proof of nf5rd 2066 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> ( ps -> A. x ps ) )
Theorem	alimdOLD 2191	Obsolete proof of alimd 2081 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	alrimiOLD 2192	Obsolete proof of alrimi 2082 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	nfdOLD 2193	Obsolete proof of nf5d 2118 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	nfdhOLD 2194	Obsolete proof of nf5dh 2026 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	alrimddOLD 2195	Obsolete proof of alrimdd 2083 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	alrimdOLD 2196	Obsolete proof of alrimd 2084 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	eximdOLD 2197	Obsolete proof of eximd 2085 as of 6-Oct-2021. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	nexdOLD 2198	Obsolete proof of nexd 2089 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> -. ps )   =>    |- ( ph -> -. E. x ps )
Theorem	albidOLD 2199	Obsolete proof of albid 2090 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )
Theorem	exbidOLD 2200	Obsolete proof of exbid 2091 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. x ch ) )