P. 23 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2201-2300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfbidfOLD 2201	Obsolete proof of nfbidf 2092 as of 6-Oct-2021. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( F/ x ps <-> F/ x ch ) )
Theorem	19.3OLD 2202	Obsolete proof of 19.3 2069 as of 6-Oct-2021. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- ( A. x ph <-> ph )
Theorem	19.9dOLD 2203	Obsolete proof of 19.9d 2070 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ps -> F/ x ph )   =>    |- ( ps -> ( E. x ph -> ph ) )
Theorem	19.9tOLD 2204	Obsolete proof of 19.9t 2071 as of 6-Oct-2021. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) (Proof shortened by Wolf Lammen, 14-Jul-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( E. x ph <-> ph ) )
Theorem	19.9OLD 2205	Obsolete proof of 19.9 2072 as of 6-Oct-2021. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- ( E. x ph <-> ph )
Theorem	19.9hOLD 2206	Obsolete proof of 19.9h 2120 as of 6-Oct-2021. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 5-Jan-2018.) (Proof shortened by Wolf Lammen, 14-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( E. x ph <-> ph )
Theorem	nfa1OLDOLD 2207	Obsolete proof of nfa1 2028 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x A. x ph
Theorem	nfnf1OLDOLD 2208	Obsolete proof of nfnf1 2031 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x F/ x ph
Theorem	nfntOLD 2209	Obsolete proof of nfnt 1782 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( F/ x ph -> F/ x -. ph )
Theorem	nfnOLD 2210	Obsolete proof of nfn 1784 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- F/ x -. ph
Theorem	nfndOLD 2211	Obsolete proof of nfnd 1785 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	19.21t-1OLD 2212	One direction of the bi-conditional in 19.21t 2073. Unlike the reverse implication, it does not depend on ax-10 2019. Obsolete as of 6-Oct-2021 (Contributed by Wolf Lammen, 4-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) )
Theorem	19.21tOLD 2213	Obsolete proof of 19.21t 2073 as of 6-Oct-2021. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	19.21OLD 2214	Obsolete proof of 19.21 2075 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	19.21-2OLD 2215	Obsolete proof of 19.21-2 2078 as of 6-Oct-2021. (Contributed by NM, 4-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ y ph   =>    |- ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps ) )
Theorem	19.21hOLD 2216	Obsolete proof of 19.21h 2121 as of 6-Oct-2021. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	stdpc5OLDOLD 2217	Obsolete proof of stdpc5 2076 as of 6-Oct-2021. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 4-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
Theorem	19.23tOLD 2218	Obsolete proof of 19.23t 2079 as of 6-Oct-2021. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F/ x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	19.23OLD 2219	Obsolete proof of 19.23 2080 as of 6-Oct-2021. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.23hOLD 2220	Obsolete proof of 19.23h 2122 as of 6-Oct-2021. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ps -> A. x ps )   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	exlimiOLD 2221	Obsolete proof of exlimi 2086 as of 6-Oct-2021. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimihOLD 2222	Obsolete proof of exlimih 2148 as of 6-Oct-2021. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimdOLD 2223	Obsolete proof of exlimd 2087 as of 6-Oct-2021. (Contributed by NM, 23-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimdhOLD 2224	Obsolete proof of exlimdh 2149 as of 6-Oct-2021. (Contributed by NM, 28-Jan-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ch -> A. x ch )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	nfdiOLD 2225	Obsolete proof of nf5di 2119 as of 6-Oct-2021. (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/ x ph )   =>    |- F/ x ph
Theorem	nfimdOLD 2226	Obsolete proof of nfimd 1823 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps -> ch ) )
Theorem	hbim1OLD 2227	Obsolete proof of hbim 2127 as of 6-Oct-2021. (Contributed by NM, 2-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1OLD 2228	Obsolete proof of nfim1 2067 as of 6-Oct-2021. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph -> ps )
Theorem	nfimOLD 2229	Obsolete proof of nfim 1825 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -> ps )
Theorem	hbimdOLD 2230	Obsolete proof of hbimd 2126 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
Theorem	hbimOLD 2231	Obsolete proof of hbim 2127 as of 6-Oct-2021. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfandOLD 2232	Obsolete proof of nfand 1826 as of 6-Oct-2021. (Contributed by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps /\ ch ) )
Theorem	nf3andOLD 2233	Obsolete proof of nf3and 1827 as of 6-Oct-2021. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/ x th )   =>    |- ( ph -> F/ x ( ps /\ ch /\ th ) )
Theorem	19.27OLD 2234	Obsolete proof of 19.27 2095 as of 6-Oct-2021. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28OLD 2235	Obsolete proof of 19.28 2096 as of 6-Oct-2021. (Contributed by NM, 1-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	nfan1OLD 2236	Obsolete proof of nfan1 2068 as of 6-Oct-2021. (Contributed by Mario Carneiro, 3-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfanOLDOLD 2237	Obsolete proof of nfan 1828 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph /\ ps )
Theorem	nfnanOLD 2238	Obsolete proof of nfnan 1830 as of 6-Oct-2021. (Contributed by Scott Fenton, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -/\ ps )
Theorem	nf3anOLD 2239	Obsolete proof of nf3an 1831 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph /\ ps /\ ch )
Theorem	hbanOLD 2240	Obsolete proof of hban 2128 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
Theorem	hb3anOLD 2241	Obsolete proof of hb3an 2129 as of 6-Oct-2021. (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
Theorem	nfbidOLD 2242	Obsolete proof of nfbid 1832 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps <-> ch ) )
Theorem	nfbiOLD 2243	Obsolete proof of nfbi 1833 as of 6-Oct-2021. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph <-> ps )
Theorem	nforOLD 2244	Obsolete proof of nfor 1834 as of 6-Oct-2021. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph \/ ps )
Theorem	nf3orOLD 2245	Obsolete proof of nf3or 1835 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph \/ ps \/ ch )
1.5.4  Axiom scheme ax-13 (Quantified Equality)
Axiom	ax-13 2246	Axiom of Quantified Equality. One of the equality and substitution axioms of predicate calculus with equality. An equivalent way to express this axiom that may be easier to understand is ( -. x = y -> ( -. x = z -> ( y = z -> A. x y = z ) ) ) (see ax13b 1964). Recall that in the intended interpretation, our variables are metavariables ranging over the variables of predicate calculus (the object language). In order for the first antecedent -. x = y to hold, x and y must have different values and thus cannot be the same object-language variable (so they are effectively "distinct variables" even though no $d is present). Similarly, x and z cannot be the same object-language variable. Therefore, x will not occur in the wff y = z when the first two antecedents hold, so analogous to ax-5 1839, the conclusion ( y = z -> A. x y = z ) follows. Note that ax-5 1839 cannot prove this because its distinct variable ($d) requirement is not satisfied directly but only indirectly (outside of Metamath) by the argument above. The original version of this axiom was ax-c9 34175 and was replaced with this shorter ax-13 2246 in December 2015. The old axiom is proved from this one as theorem axc9 2302. The primary purpose of this axiom is to provide a way to introduce the quantifier A. x on y = z even when x and y are substituted with the same variable. In this case, the first antecedent becomes -. x = x and the axiom still holds. Although this version is shorter, the original version axc9 2302 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2302 is in dvelimh 2336 which converts a distinct variable pair to the distinctor antecedent -. A. x x = y. In particular, it is conjectured that it is not possible to prove ax6 2251 from ax6v 1889 without this axiom. This axiom can be weakened if desired by adding distinct variable restrictions on pairs x , z and y , z. To show that, we add these restrictions to theorem ax13v 2247 and use only ax13v 2247 for further derivations. Thus, ax13v 2247 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2247 (preferred) or ax13 2249 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2013) but is used as an auxiliary axiom scheme to achieve scheme completeness (i.e. so that all possible cases of bundling can be proved; see text linked at mmtheorems.html#ax6dgen). It is not known whether this axiom can be derived from the others. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.)
|- ( -. x = y -> ( y = z -> A. x y = z ) )
Theorem	ax13v 2247*	A weaker version of ax-13 2246 with distinct variable restrictions on pairs x , z and y , z. In order to show (with ax13 2249) that this weakening is still adequate, this should be the only theorem referencing ax-13 2246 directly. Had we additionally required x and y be distinct, too, this theorem would have been a direct consequence of ax-5 1839. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. (Contributed by NM, 30-Jun-2016.)
|- ( -. x = y -> ( y = z -> A. x y = z ) )
Theorem	ax13lem1 2248*	A version of ax13v 2247 with one distinct variable restriction dropped. For convenience, y is kept on the right side of equations. The proof of ax13 2249 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
|- ( -. x = y -> ( z = y -> A. x z = y ) )
Theorem	ax13 2249	Derive ax-13 2246 from ax13v 2247 and Tarski's FOL. This shows that the weakening in ax13v 2247 is still sufficient for a complete system. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) Reduce axiom usage (Revised by Wolf Lammen, 2-Jun-2021.)
|- ( -. x = y -> ( y = z -> A. x y = z ) )
Theorem	ax6e 2250	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-4 1737 through ax-9 1999, all axioms other than ax-6 1888 are believed to be theorems of free logic, although the system without ax-6 1888 is not complete in free logic. It is preferred to use ax6ev 1890 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2248 became available. (Revised by Wolf Lammen, 8-Sep-2018.)
|- E. x x = y
Theorem	ax6 2251	Theorem showing that ax-6 1888 follows from the weaker version ax6v 1889. (Even though this theorem depends on ax-6 1888, all references of ax-6 1888 are made via ax6v 1889. An earlier version stated ax6v 1889 as a separate axiom, but having two axioms caused some confusion.) This theorem should be referenced in place of ax-6 1888 so that all proofs can be traced back to ax6v 1889. When possible, use the weaker ax6v 1889 rather than ax6 2251 since the ax6v 1889 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.)
|- -. A. x -. x = y
Theorem	axc10 2252	Show that the original axiom ax-c10 34171 can be derived from ax6 2251 and axc7 2132 (on top of propositional calculus, ax-gen 1722, and ax-4 1737). See ax6fromc10 34181 for the rederivation of ax6 2251 from ax-c10 34171. Normally, axc10 2252 should be used rather than ax-c10 34171, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Theorem	spimt 2253	Closed theorem form of spim 2254. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Feb-2018.)
|- ( ( F/ x ps /\ A. x ( x = y -> ( ph -> ps ) ) ) -> ( A. x ph -> ps ) )
Theorem	spim 2254	Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2254 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spimed 2255	Deduction version of spime 2256. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.)
|- ( ch -> F/ x ph )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ch -> ( ph -> E. x ps ) )
Theorem	spime 2256	Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.)
|- F/ x ph   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	spimv 2257*	A version of spim 2254 with a distinct variable requirement instead of a bound variable hypothesis. See also spimv1 2115 and spimvw 1927. See also spimvALT 2258. (Contributed by NM, 31-Jul-1993.) Removed dependency on ax-10 2019. (Revised by BJ, 29-Nov-2020.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spimvALT 2258*	Alternate proof of spimv 2257. Shorter but requires more axioms. (Contributed by NM, 31-Jul-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spimev 2259*	Distinct-variable version of spime 2256. (Contributed by NM, 10-Jan-1993.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	spv 2260*	Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spei 2261	Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ps   =>    |- E. x ph
Theorem	chvar 2262	Implicit substitution of y for x into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	chvarv 2263*	Implicit substitution of y for x into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 14-Jul-2021.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	chvarvOLD 2264*	Obsolete proof of chvarv 2263 as of 14-Jul-2021. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	cbv3 2265	Rule used to change bound variables, using implicit substitution, that does not use ax-c9 34175. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	cbv3h 2266	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.)
|- ( ph -> A. y ph )   &    |- ( ps -> A. x ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	cbv1 2267	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x = y -> ( ps -> ch ) ) )   =>    |- ( ph -> ( A. x ps -> A. y ch ) )
Theorem	cbv1h 2268	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.)
|- ( ph -> ( ps -> A. y ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   &    |- ( ph -> ( x = y -> ( ps -> ch ) ) )   =>    |- ( A. x A. y ph -> ( A. x ps -> A. y ch ) )
Theorem	cbv2h 2269	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 11-May-1993.)
|- ( ph -> ( ps -> A. y ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )
Theorem	cbv2 2270	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	cbval 2271	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvex 2272	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	cbvalv 2273*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 17-Jul-2021.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvalvOLD 2274*	Obsolete proof of cbvalv 2273 as of 17-Jul-2021. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvexv 2275*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 17-Jul-2021.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	cbvexvOLD 2276*	Obsolete proof of cbvexv 2275 as of 17-Jul-2021. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	cbvald 2277*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2337. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
|- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	cbvexd 2278*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2337. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	cbval2 2279*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	cbvex2 2280*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	cbvaldva 2281*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	cbvaldvaOLD 2282*	Obsolete proof of cbvaldva 2281 as of 18-Jul-2021. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	cbvexdva 2283*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	cbvexdvaOLD 2284*	Obsolete proof of cbvexdva 2283 as of 18-Jul-2021. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	cbval2v 2285*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	cbval2vOLD 2286*	Obsolete proof of cbval2v 2285 as of 18-Jul-2021. (Contributed by NM, 4-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	cbvex2v 2287*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	cbvex2vOLD 2288*	Obsolete proof of cbvex2v 2287 as of 18-Jul-2021. (Contributed by NM, 26-Jul-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	cbvex4v 2289*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
|- ( ( x = v /\ y = u ) -> ( ph <-> ps ) )   &    |- ( ( z = f /\ w = g ) -> ( ps <-> ch ) )   =>    |- ( E. x E. y E. z E. w ph <-> E. v E. u E. f E. g ch )
Theorem	equs4 2290	Lemma used in proofs of implicit substitution properties. The converse requires either a dv condition (sb56 2150) or a non-freeness hypothesis (equs45f 2350). See equs4v 1930 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.)
|- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
Theorem	equsal 2291	An equivalence related to implicit substitution. See equsalvw 1931 and equsalv 2108 for versions with dv conditions proved from fewer axioms. See also the dual form equsex 2292. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	equsex 2292	An equivalence related to implicit substitution. See equsexvw 1932 and equsexv 2109 for versions with dv conditions proved from fewer axioms. See also the dual form equsal 2291. See equsexALT 2293 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	equsexALT 2293	Alternate proof of equsex 2292. This proves the result directly, instead of as a corollary of equsal 2291 via equs4 2290. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2246 is ax6e 2250. This proof mimics that of equsal 2291 (in particular, note that pm5.32i 669, exbii 1774, 19.41 2103, mpbiran 953 correspond respectively to pm5.74i 260, albii 1747, 19.23 2080, a1bi 352). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	equsalh 2294	An equivalence related to implicit substitution. See equsalhw 2123 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	equsexh 2295	An equivalence related to implicit substitution. See equsexhv 2124 for a version with a dv condition which does not require ax-13 2246. (Contributed by NM, 5-Aug-1993.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	ax13lem2 2296*	Lemma for nfeqf2 2297. This lemma is equivalent to ax13v 2247 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020.) (New usage is discouraged.)
|- ( -. x = y -> ( E. x z = y -> z = y ) )
Theorem	nfeqf2 2297*	An equation between setvar is free of any other setvar. (Contributed by Wolf Lammen, 9-Jun-2019.)
|- ( -. A. x x = y -> F/ x z = y )
Theorem	dveeq2 2298*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 8-Sep-2018.)
|- ( -. A. x x = y -> ( z = y -> A. x z = y ) )
Theorem	nfeqf1 2299*	An equation between setvar is free of any other setvar. (Contributed by Wolf Lammen, 10-Jun-2019.)
|- ( -. A. x x = y -> F/ x y = z )
Theorem	dveeq1 2300*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 8-Sep-2018.)
|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )