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	hbal 2201	If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	hbald 2202	Deduction form of bound-variable hypothesis builder hbal 2201. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
Theorem	sbal 2203*	Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 13-Aug-2023.)
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbalv 2204*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥]∀𝑧𝜑 ↔ ∀𝑧𝜓)
Theorem	hbsbw 2205*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Version of hbsb 2555 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 12-Aug-1993.) Remove dependencies on axioms. (Revised by GG, 23-May-2024.) (Proof shortened by Wolf Lammen, 14-May-2025.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbcom2 2206*	Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 23-Dec-2022.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sbco4lemOLD 2207*	Obsolete version of sbco4lem 2135 as of 3-Sep-2025. (Contributed by Jim Kingdon, 26-Sep-2018.) (Proof shortened by Wolf Lammen, 12-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbco4OLD 2208*	Obsolete version of sbco4 2136 as of 3-Sep-2025. (Contributed by Jim Kingdon, 25-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑢][𝑥 / 𝑣][𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	nfa2 2209	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) Remove dependency on ax-12 2212. (Revised by Wolf Lammen, 18-Oct-2021.)
⊢ Ⅎ𝑥∀𝑦∀𝑥𝜑
Theorem	nfexhe 2210	Version of nfex 2356 with the existential dual to the 'h' hypothesis, avoiding ax-12 2212. (Contributed by SN, 11-Feb-2026.)
⊢ (∃𝑥𝜑 → 𝜑)    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	nfexa2 2211	An inner universal quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
⊢ Ⅎ𝑥∃𝑦∀𝑥𝜑
1.5.3  Axiom scheme ax-12 (Substitution)
Axiom	ax-12 2212	Axiom of Substitution. One of the 5 equality axioms of predicate calculus. The final consequent ∀𝑥(𝑥 = 𝑦 → 𝜑) is a way of expressing "𝑦 substituted for 𝑥 in wff 𝜑 " (cf. sb6 2118). 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 39691 and was replaced with this shorter ax-12 2212 in Jan. 2007. The old axiom is proved from this one as Theorem axc15 2453. Conversely, this axiom is proved from ax-c15 39691 as Theorem ax12 2454. Juha Arpiainen proved the metalogical independence of this axiom (in the form of the older axiom ax-c15 39691) from the others on 19-Jan-2006. See item 9a at https://us.metamath.org/award2003.html 39691. See ax12v 2213 and ax12v2 2214 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions. This axiom scheme is logically redundant (see ax12w 2167) but is used as an auxiliary axiom scheme to achieve scheme completeness. (Contributed by NM, 22-Jan-2007.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12v 2213*	This is essentially Axiom ax-12 2212 weakened by additional restrictions on variables. Besides axc11r 2399, this theorem should be the only one referencing ax-12 2212 directly. Both restrictions on variables have their own value. If for a moment we assume 𝑥 could be set to 𝑦, then, after elimination of the tautology 𝑦 = 𝑦, immediately we have 𝜑 → ∀𝑦𝜑 for all 𝜑 and 𝑦, that is ax-5 1939, a degenerate result. The second restriction is not necessary, but a simplification that makes the following interpretation easier to see. Since 𝜑 textually at most depends on 𝑥, we can look at it at some given 'fixed' 𝑦. This theorem now states that the truth value of 𝜑 will stay constant, as long as we 'vary 𝑥 around 𝑦' only such that 𝑥 = 𝑦 still holds. Or in other words, equality is the finest grained logical expression. If you cannot differ two sets by =, you won't find a whatever sophisticated expression that does. One might wonder how the described variation of 𝑥 is possible at all. Note that Metamath is a text processor that easily sees a difference between text chunks {𝑥 ∣ ¬ 𝑥 = 𝑥} and {𝑦 ∣ ¬ 𝑦 = 𝑦}. Our usual interpretation is to abstract from textual variations of the same set, but we are free to interpret Metamath's formalism differently, and in fact let 𝑥 run through all textual representations of sets. Had we allowed 𝜑 to depend also on 𝑦, this idea is both harder to see, and it is less clear that this extra freedom introduces effects not covered by other axioms. (Contributed by Wolf Lammen, 8-Aug-2020.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12v2 2214*	It is possible to remove any restriction on 𝜑 in ax12v 2213. Same as Axiom C8 of [Monk2] p. 105. Use ax12v 2213 instead when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-10 2175 and ax-13 2403. (Revised by Jim Kingdon, 15-Dec-2017.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12ev2 2215*	Version of ax12v2 2214 rewritten to use an existential quantifier. One direction of sbalex 2277 without the universal quantifier, avoiding ax-10 2175. (Contributed by SN, 14-Aug-2025.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 → 𝜑))
Theorem	19.8a 2216	If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v 2012 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2218. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	19.8ad 2217	If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2216. (Contributed by DAW, 13-Feb-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	sp 2218	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). This corresponds to the axiom (T) of modal logic. For the axiom of specialization presented in many logic textbooks, see Theorem stdpc4 2101. This theorem shows that our obsolete axiom ax-c5 39685 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 2212. It is thought the best we can do using only Tarski's axioms is spw 2063. Also see spvw 2010 where 𝑥 and 𝜑 are disjoint, using fewer axioms. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	spi 2219	Inference rule of universal instantiation, or universal specialization. Converse of the inference rule of (universal) generalization ax-gen 1824. Contrary to the rule of generalization, its closed form is valid, see sp 2218. (Contributed by NM, 5-Aug-1993.)
⊢ ∀𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	sps 2220	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	2sp 2221	A double specialization (see sp 2218). Another double specialization, closer to PM*11.1, is 2stdpc4 2103. (Contributed by BJ, 15-Sep-2018.)
⊢ (∀𝑥∀𝑦𝜑 → 𝜑)
Theorem	spsd 2222	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	19.2g 2223	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. Use 19.2 2005 when sufficient. (Contributed by Mel L. O'Cat, 31-Mar-2008.)
⊢ (∀𝑥𝜑 → ∃𝑦𝜑)
Theorem	19.21bi 2224	Inference form of 19.21 2242 and also deduction form of sp 2218. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.21bbi 2225	Inference removing two universal quantifiers. Version of 19.21bi 2224 with two quantifiers. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → ∀𝑥∀𝑦𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.23bi 2226	Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2246. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	nexr 2227	Inference associated with the contrapositive of 19.8a 2216. (Contributed by Jeff Hankins, 26-Jul-2009.)
⊢ ¬ ∃𝑥𝜑    ⇒   ⊢ ¬ 𝜑
Theorem	qexmid 2228	Quantified excluded middle (see exmid 907). Also known as the drinker paradox (if 𝜑(𝑥) is interpreted as "𝑥 drinks", then this theorem tells that there exists a person such that, if this person drinks, then everyone drinks). Exercise 9.2a of Boolos, p. 111, Computability and Logic. (Contributed by NM, 10-Dec-2000.)
⊢ ∃𝑥(𝜑 → ∀𝑥𝜑)
Theorem	nf5r 2229	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) df-nf 1813 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 23-Nov-2023.)
⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	nf5ri 2230	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nf5rd 2231	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	spimedv 2232*	Deduction version of spimev 2423. Version of spimed 2419 with a disjoint variable condition, which does not require ax-13 2403. See spime 2420 for a non-deduction version. (Contributed by NM, 14-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝜒 → Ⅎ𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓))
Theorem	spimefv 2233*	Version of spime 2420 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	nfim1 2234	A closed form of nfim 1925. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1813 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfan1 2235	A closed form of nfan 1928. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1813 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	19.3t 2236	Closed form of 19.3 2237 and version of 19.9t 2239 with a universal quantifier. (Contributed by NM, 9-Nov-2020.) (Proof shortened by BJ, 9-Oct-2022.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥𝜑 ↔ 𝜑))
Theorem	19.3 2237	A wff may be quantified with a variable not free in it. Version of 19.9 2240 with a universal quantifier. Theorem 19.3 of [Margaris] p. 89. See 19.3v 2011 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.9d 2238	A deduction version of one direction of 19.9 2240. (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.) df-nf 1813 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
⊢ (𝜓 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	19.9t 2239	Closed form of 19.9 2240 and version of 19.3t 2236 with an existential quantifier. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 14-Jul-2020.)
⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 ↔ 𝜑))
Theorem	19.9 2240	A wff may be existentially quantified with a variable not free in it. Version of 19.3 2237 with an existential quantifier. Theorem 19.9 of [Margaris] p. 89. See 19.9v 2013 for a version requiring fewer axioms. (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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	19.21t 2241	Closed form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2242. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) df-nf 1813 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 3-Nov-2021.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21 2242	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See 19.21v 1968 for a version requiring fewer axioms. See also 19.21h 2321. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) df-nf 1813 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	stdpc5 2243	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎ𝑥𝜑 can be thought of as emulating "𝑥 is not free in 𝜑". With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example 𝑥 would not (for us) be free in 𝑥 = 𝑥 by nfequid 2042. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. See stdpc5v 1967 for a version requiring fewer axioms. (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 2175. (Revised by Wolf Lammen, 4-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	19.21-2 2244	Version of 19.21 2242 with two quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	19.23t 2245	Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23 2246. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) df-nf 1813 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	19.23 2246	Theorem 19.23 of [Margaris] p. 90. See 19.23v 1971 for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	alimd 2247	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1839. See alimdh 1846, alimdv 1945 for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alrimi 2248	Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2242. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	alrimdd 2249	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2242. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 2250	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2242. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximd 2251	Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1863. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	exlimi 2252	Inference associated with 19.23 2246. See exlimiv 1959 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exlimd 2253	Deduction form of 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.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	exlimimdd 2254	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2255. (Revised by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exlimdd 2255	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	nexd 2256	Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	albid 2257	Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbid 2258	Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	nfbidf 2259	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1813 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒))
Theorem	19.16 2260	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓))
Theorem	19.17 2261	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓))
Theorem	19.27 2262	Theorem 19.27 of [Margaris] p. 90. See 19.27v 2024 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28 2263	Theorem 19.28 of [Margaris] p. 90. See 19.28v 2025 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 7-May-2025.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.19 2264	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓))
Theorem	19.36 2265	Theorem 19.36 of [Margaris] p. 90. See 19.36v 2022 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓))
Theorem	19.36i 2266	Inference associated with 19.36 2265. See 19.36iv 1975 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.37 2267	Theorem 19.37 of [Margaris] p. 90. See 19.37v 2026 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.32 2268	Theorem 19.32 of [Margaris] p. 90. See 19.32v 1969 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓))
Theorem	19.31 2269	Theorem 19.31 of [Margaris] p. 90. See 19.31v 1970 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓))
Theorem	19.41 2270	Theorem 19.41 of [Margaris] p. 90. See 19.41v 1978 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.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.42 2271	Theorem 19.42 of [Margaris] p. 90. See 19.42v 1982 for a version requiring fewer axioms. See exan 1891 for an immediate version. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	19.44 2272	Theorem 19.44 of [Margaris] p. 90. See 19.44v 2027 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45 2273	Theorem 19.45 of [Margaris] p. 90. See 19.45v 2028 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	spimfv 2274*	Specialization, using implicit substitution. Version of spim 2418 with a disjoint variable condition, which does not require ax-13 2403. See spimvw 2015 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2421 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarfv 2275*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2426 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	cbv3v2 2276*	Version of cbv3 2428 with two disjoint variable conditions, which does not require ax-11 2191 nor ax-13 2403. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	sbalex 2277*	Equivalence of two ways to express proper substitution of a setvar for another setvar disjoint from it in a formula. This proof of their equivalence does not use df-sb 2096. That both sides of the biconditional express proper substitution is proved by sb5 2310 and sb6 2118. The implication "to the left" is equs4v 2029 and does not require ax-10 2175 nor ax-12 2212. It also holds without disjoint variable condition if we allow more axioms (see equs4 2447). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2491 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2490 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2303 in place of equsex 2449 in order to remove dependency on ax-13 2403. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2096. (Revised by BJ, 21-Sep-2024.) (Proof shortened by SN, 14-Aug-2025.)
⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbalexOLD 2278*	Obsolete version of sbalex 2277 as of 14-Aug-2025. (Contributed by NM, 14-Apr-2008.) (Revised by BJ, 20-Dec-2020.) (Revised by BJ, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sb4av 2279*	Version of sb4a 2511 with a disjoint variable condition, which does not require ax-13 2403. The distinctor antecedent from sb4b 2506 is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbimd 2280	Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2096. (Revised by Steven Nguyen, 9-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
Theorem	sbbid 2281	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2175 and ax-13 2403. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2096. (Revised by Steven Nguyen, 11-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	2sbbid 2282	Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒))
Theorem	sbequ1 2283	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2096. (Revised by BJ, 22-Dec-2020.)
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑))
Theorem	sbequ2 2284	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2096. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.)
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑))
Theorem	stdpc7 2285	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2057.) Translated to traditional notation, it can be read: "𝑥 = 𝑦 → (𝜑(𝑥, 𝑥) → 𝜑(𝑥, 𝑦)), provided that 𝑦 is free for 𝑥 in 𝜑(𝑥, 𝑥)". Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 → 𝜑))
Theorem	sbequ12 2286	An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Theorem	sbequ12r 2287	An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))
Theorem	sbelx 2288*	Elimination of substitution. Also see sbel2x 2505. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2403. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2175. (Revised by GG, 20-Aug-2023.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbequ12a 2289	An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.)
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑))
Theorem	sbid 2290	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.)
⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbcov 2291*	A composition law for substitution. Version of sbco 2538 with a disjoint variable condition using fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by GG, 7-Aug-2023.) (Proof shortened by SN, 26-Aug-2025.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbcovOLD 2292*	Obsolete version of sbcov 2291 as of 26-Aug-2025. (Contributed by NM, 14-May-1993.) (Revised by GG, 7-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sb6a 2293*	Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	sbid2vw 2294*	Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2540, at the expense of an extra distinct variable condition. (Contributed by NM, 14-May-1993.) (Revised by Wolf Lammen, 5-Aug-2023.)
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑)
Theorem	axc16g 2295*	Generalization of axc16 2296. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2037 }, Theorem ax12v 2213. (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 2403, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2300. (Revised by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	axc16 2296*	Proof of older axiom ax-c16 39694. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gb 2297*	Biconditional strengthening of axc16g 2295. (Contributed by NM, 15-May-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑))
Theorem	axc16nf 2298*	If dtru 5417 is false, then there is only one element in the universe, so everything satisfies Ⅎ. (Contributed by Mario Carneiro, 7-Oct-2016.) Remove dependency on ax-11 2191. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2175. (Revised by Wolf Lammen, 12-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	axc11v 2299*	Version of axc11 2461 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2037 }, from ax12v 2213 (contrary to axc11 2461 which seems to require the full ax-12 2212 and ax-13 2403). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	axc11rv 2300*	Version of axc11r 2399 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2037 }, from ax12v 2213 (contrary to axc11 2461 which seems to require the full ax-12 2212 and ax-13 2403, and to axc11r 2399 which seems to require the full ax-12 2212). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑))