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	19.21bi 2201	Inference form of 19.21 2219 and also deduction form of sp 2195. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.21bbi 2202	Inference removing two universal quantifiers. Version of 19.21bi 2201 with two quantifiers. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → ∀𝑥∀𝑦𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.23bi 2203	Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2223. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	nexr 2204	Inference associated with the contrapositive of 19.8a 2193. (Contributed by Jeff Hankins, 26-Jul-2009.)
⊢ ¬ ∃𝑥𝜑    ⇒   ⊢ ¬ 𝜑
Theorem	qexmid 2205	Quantified excluded middle (see exmid 900). 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 2206	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) df-nf 1791 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 23-Nov-2023.)
⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	nf5ri 2207	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nf5rd 2208	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	spimedv 2209*	Deduction version of spimev 2400. Version of spimed 2396 with a disjoint variable condition, which does not require ax-13 2380. See spime 2397 for a non-deduction version. (Contributed by NM, 14-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝜒 → Ⅎ𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓))
Theorem	spimefv 2210*	Version of spime 2397 with a disjoint variable condition, which does not require ax-13 2380. (Contributed by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	nfim1 2211	A closed form of nfim 1903. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1791 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfan1 2212	A closed form of nfan 1906. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1791 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	19.3t 2213	Closed form of 19.3 2214 and version of 19.9t 2216 with a universal quantifier. (Contributed by NM, 9-Nov-2020.) (Proof shortened by BJ, 9-Oct-2022.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥𝜑 ↔ 𝜑))
Theorem	19.3 2214	A wff may be quantified with a variable not free in it. Version of 19.9 2217 with a universal quantifier. Theorem 19.3 of [Margaris] p. 89. See 19.3v 1989 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.9d 2215	A deduction version of one direction of 19.9 2217. (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 1791 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
⊢ (𝜓 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	19.9t 2216	Closed form of 19.9 2217 and version of 19.3t 2213 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 2217	A wff may be existentially quantified with a variable not free in it. Version of 19.3 2214 with an existential quantifier. Theorem 19.9 of [Margaris] p. 89. See 19.9v 1991 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 2218	Closed form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2219. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) df-nf 1791 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 3-Nov-2021.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21 2219	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See 19.21v 1946 for a version requiring fewer axioms. See also 19.21h 2298. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) df-nf 1791 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	stdpc5 2220	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 2020. 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 1945 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 2152. (Revised by Wolf Lammen, 4-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	19.21-2 2221	Version of 19.21 2219 with two quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	19.23t 2222	Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23 2223. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) df-nf 1791 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	19.23 2223	Theorem 19.23 of [Margaris] p. 90. See 19.23v 1949 for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	alimd 2224	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1817. See alimdh 1824, alimdv 1923 for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alrimi 2225	Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2219. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	alrimdd 2226	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2219. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 2227	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2219. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximd 2228	Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1841. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	exlimi 2229	Inference associated with 19.23 2223. See exlimiv 1937 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 2230	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 2231	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2232. (Revised by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exlimdd 2232	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	nexd 2233	Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	albid 2234	Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbid 2235	Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	nfbidf 2236	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1791 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒))
Theorem	19.16 2237	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓))
Theorem	19.17 2238	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓))
Theorem	19.27 2239	Theorem 19.27 of [Margaris] p. 90. See 19.27v 2002 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28 2240	Theorem 19.28 of [Margaris] p. 90. See 19.28v 2003 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 7-May-2025.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.19 2241	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓))
Theorem	19.36 2242	Theorem 19.36 of [Margaris] p. 90. See 19.36v 2000 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓))
Theorem	19.36i 2243	Inference associated with 19.36 2242. See 19.36iv 1953 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.37 2244	Theorem 19.37 of [Margaris] p. 90. See 19.37v 2004 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.32 2245	Theorem 19.32 of [Margaris] p. 90. See 19.32v 1947 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓))
Theorem	19.31 2246	Theorem 19.31 of [Margaris] p. 90. See 19.31v 1948 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓))
Theorem	19.41 2247	Theorem 19.41 of [Margaris] p. 90. See 19.41v 1956 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 2248	Theorem 19.42 of [Margaris] p. 90. See 19.42v 1960 for a version requiring fewer axioms. See exan 1869 for an immediate version. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	19.44 2249	Theorem 19.44 of [Margaris] p. 90. See 19.44v 2005 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45 2250	Theorem 19.45 of [Margaris] p. 90. See 19.45v 2006 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	spimfv 2251*	Specialization, using implicit substitution. Version of spim 2395 with a disjoint variable condition, which does not require ax-13 2380. See spimvw 1993 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2398 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarfv 2252*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2403 with a disjoint variable condition, which does not require ax-13 2380. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	cbv3v2 2253*	Version of cbv3 2405 with two disjoint variable conditions, which does not require ax-11 2168 nor ax-13 2380. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	sbalex 2254*	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 2074. That both sides of the biconditional express proper substitution is proved by sb5 2287 and sb6 2096. The implication "to the left" is equs4v 2007 and does not require ax-10 2152 nor ax-12 2189. It also holds without disjoint variable condition if we allow more axioms (see equs4 2424). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2468 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2467 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2280 in place of equsex 2426 in order to remove dependency on ax-13 2380. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2074. (Revised by BJ, 21-Sep-2024.) (Proof shortened by SN, 14-Aug-2025.)
⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbalexOLD 2255*	Obsolete version of sbalex 2254 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 2256*	Version of sb4a 2488 with a disjoint variable condition, which does not require ax-13 2380. The distinctor antecedent from sb4b 2483 is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbimd 2257	Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2074. (Revised by Steven Nguyen, 9-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
Theorem	sbbid 2258	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2152 and ax-13 2380. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2074. (Revised by Steven Nguyen, 11-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	2sbbid 2259	Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒))
Theorem	sbequ1 2260	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2074. (Revised by BJ, 22-Dec-2020.)
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑))
Theorem	sbequ2 2261	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2074. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.)
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑))
Theorem	stdpc7 2262	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2035.) 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 2263	An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Theorem	sbequ12r 2264	An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))
Theorem	sbelx 2265*	Elimination of substitution. Also see sbel2x 2482. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2380. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2152. (Revised by GG, 20-Aug-2023.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbequ12a 2266	An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.)
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑))
Theorem	sbid 2267	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 2268*	A composition law for substitution. Version of sbco 2515 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 2269*	Obsolete version of sbcov 2268 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 2270*	Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	sbid2vw 2271*	Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2517, at the expense of an extra distinct variable condition. (Contributed by NM, 14-May-1993.) (Revised by Wolf Lammen, 5-Aug-2023.)
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑)
Theorem	axc16g 2272*	Generalization of axc16 2273. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2015 }, Theorem ax12v 2190. (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 2380, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2277. (Revised by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	axc16 2273*	Proof of older axiom ax-c16 39385. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gb 2274*	Biconditional strengthening of axc16g 2272. (Contributed by NM, 15-May-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑))
Theorem	axc16nf 2275*	If dtru 5383 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 2168. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2152. (Revised by Wolf Lammen, 12-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	axc11v 2276*	Version of axc11 2438 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2015 }, from ax12v 2190 (contrary to axc11 2438 which seems to require the full ax-12 2189 and ax-13 2380). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	axc11rv 2277*	Version of axc11r 2376 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2015 }, from ax12v 2190 (contrary to axc11 2438 which seems to require the full ax-12 2189 and ax-13 2380, and to axc11r 2376 which seems to require the full ax-12 2189). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑))
Theorem	drsb2 2278	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	equsalv 2279*	An equivalence related to implicit substitution. Version of equsal 2425 with a disjoint variable condition, which does not require ax-13 2380. See equsalvw 2011 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2280. (Contributed by NM, 2-Jun-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexv 2280*	An equivalence related to implicit substitution. Version of equsex 2426 with a disjoint variable condition, which does not require ax-13 2380. See equsexvw 2012 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2279. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid ax-10 2152. (Revised by GG, 18-Nov-2024.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	sbft 2281	Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbf 2282	Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2099. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbf2 2283	Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	sbh 2284	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	hbs1 2285*	The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1f 2286	If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sb5 2287*	Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v 2098 and even needs no disjoint variable condition, see sb1 2486. Theorem sb5f 2506 replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Revised by Wolf Lammen, 4-Sep-2023.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	equs5av 2288*	A property related to substitution that replaces the distinctor from equs5 2468 to a disjoint variable condition. Version of equs5a 2465 with a disjoint variable condition, which does not require ax-13 2380. See also sbalex 2254. (Contributed by NM, 2-Feb-2007.) (Revised by GG, 15-Dec-2023.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2sb5 2289*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑))
Theorem	dfsb7 2290*	An alternate definition of proper substitution df-sb 2074. By introducing a dummy variable 𝑦 in the definiens, we are able to eliminate any distinct variable restrictions among the variables 𝑡, 𝑥, and 𝜑 of the definiendum. No distinct variable conflicts arise because 𝑦 effectively insulates 𝑡 from 𝑥. To achieve this, we use a chain of two substitutions in the form of sb5 2287, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2719. Theorem sb7h 2534 provides a version where 𝜑 and 𝑦 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2074. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	sbn 2291	Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) Revise df-sb 2074. (Revised by BJ, 25-Dec-2020.)
⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑)
Theorem	sbex 2292*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.)
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
Theorem	nf5 2293	Alternate definition of df-nf 1791. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1791 changed. (Revised by Wolf Lammen, 11-Sep-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
Theorem	nf6 2294	An alternate definition of df-nf 1791. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	nf5d 2295	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	nf5di 2296	Since the converse holds by a1i 11, this inference shows that we can represent a not-free hypothesis with either Ⅎ𝑥𝜑 (inference form) or (𝜑 → Ⅎ𝑥𝜑) (deduction form). (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.)
⊢ (𝜑 → Ⅎ𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	19.9h 2297	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.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	19.21h 2298	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2219 and 19.21v 1946. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	19.23h 2299	Theorem 19.23 of [Margaris] p. 90. See 19.23 2223. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	exlimih 2300	Inference associated with 19.23 2223. See exlimiv 1937 for a version with a disjoint variable 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.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)