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.21 2201	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See 19.21v 1943 for a version requiring fewer axioms. See also 19.21h 2284. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	stdpc5 2202	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 2017. 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 1942 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 2138. (Revised by Wolf Lammen, 4-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	19.21-2 2203	Version of 19.21 2201 with two quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	19.23t 2204	Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23 2205. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) df-nf 1787 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	19.23 2205	Theorem 19.23 of [Margaris] p. 90. See 19.23v 1946 for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	alimd 2206	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1813. See alimdh 1820, alimdv 1920 for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alrimi 2207	Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2201. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	alrimdd 2208	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2201. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 2209	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2201. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximd 2210	Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1837. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	exlimi 2211	Inference associated with 19.23 2205. See exlimiv 1934 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 2212	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 2213	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2214. (Revised by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exlimdd 2214	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	nexd 2215	Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	albid 2216	Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbid 2217	Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	nfbidf 2218	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒))
Theorem	19.16 2219	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓))
Theorem	19.17 2220	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓))
Theorem	19.27 2221	Theorem 19.27 of [Margaris] p. 90. See 19.27v 1994 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28 2222	Theorem 19.28 of [Margaris] p. 90. See 19.28v 1995 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.19 2223	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓))
Theorem	19.36 2224	Theorem 19.36 of [Margaris] p. 90. See 19.36v 1992 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓))
Theorem	19.36i 2225	Inference associated with 19.36 2224. See 19.36iv 1951 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.37 2226	Theorem 19.37 of [Margaris] p. 90. See 19.37v 1996 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.32 2227	Theorem 19.32 of [Margaris] p. 90. See 19.32v 1944 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓))
Theorem	19.31 2228	Theorem 19.31 of [Margaris] p. 90. See 19.31v 1945 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓))
Theorem	19.41 2229	Theorem 19.41 of [Margaris] p. 90. See 19.41v 1954 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 2230	Theorem 19.42 of [Margaris] p. 90. See 19.42v 1958 for a version requiring fewer axioms. See exan 1866 for an immediate version. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	19.44 2231	Theorem 19.44 of [Margaris] p. 90. See 19.44v 1997 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45 2232	Theorem 19.45 of [Margaris] p. 90. See 19.45v 1998 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	spimfv 2233*	Specialization, using implicit substitution. Version of spim 2387 with a disjoint variable condition, which does not require ax-13 2372. See spimvw 2000 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2390 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarfv 2234*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2395 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	cbv3v2 2235*	Version of cbv3 2397 with two disjoint variable conditions, which does not require ax-11 2155 nor ax-13 2372. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	sbalex 2236*	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 2069. That both sides of the biconditional express proper substitution is proved by sb5 2268 and sb6 2089. The implication "to the left" is equs4v 2004 and does not require ax-10 2138 nor ax-12 2172. It also holds without disjoint variable condition if we allow more axioms (see equs4 2416). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2460 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2459 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2260 in place of equsex 2418 in order to remove dependency on ax-13 2372. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2069. (Revised by BJ, 21-Sep-2024.)
⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sb4av 2237*	Version of sb4a 2480 with a disjoint variable condition, which does not require ax-13 2372. The distinctor antecedent from sb4b 2475 is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbimd 2238	Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2069. (Revised by Steven Nguyen, 9-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
Theorem	sbbid 2239	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2138 and ax-13 2372. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2069. (Revised by Steven Nguyen, 11-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	2sbbid 2240	Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒))
Theorem	sbequ1 2241	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2069. (Revised by BJ, 22-Dec-2020.)
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑))
Theorem	sbequ2 2242	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2069. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.)
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑))
Theorem	stdpc7 2243	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2032.) 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 2244	An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Theorem	sbequ12r 2245	An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))
Theorem	sbelx 2246*	Elimination of substitution. Also see sbel2x 2474. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2372. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2138. (Revised by Gino Giotto, 20-Aug-2023.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbequ12a 2247	An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.)
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑))
Theorem	sbid 2248	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 2249*	A composition law for substitution. Version of sbco 2507 with a disjoint variable condition using fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Gino Giotto, 7-Aug-2023.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sb6a 2250*	Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	sbid2vw 2251*	Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2509, at the expense of an extra distinct variable condition. (Contributed by NM, 14-May-1993.) (Revised by Wolf Lammen, 5-Aug-2023.)
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑)
Theorem	axc16g 2252*	Generalization of axc16 2253. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2012 }, Theorem ax12v 2173. (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 2372, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2257. (Revised by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	axc16 2253*	Proof of older axiom ax-c16 37751. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gb 2254*	Biconditional strengthening of axc16g 2252. (Contributed by NM, 15-May-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑))
Theorem	axc16nf 2255*	If dtru 5436 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 2155. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2138. (Revised by Wolf Lammen, 12-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	axc11v 2256*	Version of axc11 2430 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2012 }, from ax12v 2173 (contrary to axc11 2430 which seems to require the full ax-12 2172 and ax-13 2372). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	axc11rv 2257*	Version of axc11r 2366 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2012 }, from ax12v 2173 (contrary to axc11 2430 which seems to require the full ax-12 2172 and ax-13 2372, and to axc11r 2366 which seems to require the full ax-12 2172). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑))
Theorem	drsb2 2258	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 2259*	An equivalence related to implicit substitution. Version of equsal 2417 with a disjoint variable condition, which does not require ax-13 2372. See equsalvw 2008 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2260. (Contributed by NM, 2-Jun-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexv 2260*	An equivalence related to implicit substitution. Version of equsex 2418 with a disjoint variable condition, which does not require ax-13 2372. See equsexvw 2009 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2259. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid ax-10 2138. (Revised by Gino Giotto, 18-Nov-2024.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	equsexvOLD 2261*	Obsolete version of equsexv 2260 as of 18-Nov-2024. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	sbft 2262	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 2263	Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2092. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbf2 2264	Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	sbh 2265	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	hbs1 2266*	The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1f 2267	If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sb5 2268*	Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v 2091 and even needs no disjoint variable condition, see sb1 2478. Theorem sb5f 2498 replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Revised by Wolf Lammen, 4-Sep-2023.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sb5OLD 2269*	Obsolete version of sb5 2268 as of 21-Sep-2024. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sb56OLD 2270*	Obsolete version of sbalex 2236 as of 21-Sep-2024. Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct, namely, alternate definitions sb5 2268 and sb6 2089. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 2069. The implication "to the left" is equs4 2416 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v 2004, requires fewer axioms). Theorem equs45f 2459 replaces the disjoint variable condition with a nonfreeness hypothesis and equs5 2460 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2260 in place of equsex 2418 in order to remove dependency on ax-13 2372. (Revised by BJ, 20-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5av 2271*	A property related to substitution that replaces the distinctor from equs5 2460 to a disjoint variable condition. Version of equs5a 2457 with a disjoint variable condition, which does not require ax-13 2372. See also sbalex 2236. (Contributed by NM, 2-Feb-2007.) (Revised by Gino Giotto, 15-Dec-2023.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2sb5 2272*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑))
Theorem	sbco4lem 2273*	Lemma for sbco4 2275. It replaces the temporary variable 𝑣 with another temporary variable 𝑤. (Contributed by Jim Kingdon, 26-Sep-2018.) (Proof shortened by Wolf Lammen, 12-Oct-2024.)
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbco4lemOLD 2274*	Obsolete version of sbco4lem 2273 as of 12-Oct-2024. (Contributed by Jim Kingdon, 26-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbco4 2275*	Two ways of exchanging two variables. Both sides of the biconditional exchange 𝑥 and 𝑦, either via two temporary variables 𝑢 and 𝑣, or a single temporary 𝑤. (Contributed by Jim Kingdon, 25-Sep-2018.)
⊢ ([𝑦 / 𝑢][𝑥 / 𝑣][𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	dfsb7 2276*	An alternate definition of proper substitution df-sb 2069. 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 2268, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2711. Theorem sb7h 2526 provides a version where 𝜑 and 𝑦 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2069. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	sbn 2277	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 2069. (Revised by BJ, 25-Dec-2020.)
⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑)
Theorem	sbex 2278*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.)
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
Theorem	nf5 2279	Alternate definition of df-nf 1787. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 11-Sep-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
Theorem	nf6 2280	An alternate definition of df-nf 1787. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	nf5d 2281	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	nf5di 2282	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 2283	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 2284	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2201 and 19.21v 1943. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	19.23h 2285	Theorem 19.23 of [Margaris] p. 90. See 19.23 2205. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	exlimih 2286	Inference associated with 19.23 2205. See exlimiv 1934 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.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exlimdh 2287	Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	equsalhw 2288*	Version of equsalh 2420 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexhv 2289*	An equivalence related to implicit substitution. Version of equsexh 2421 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	hba1 2290	The setvar 𝑥 is not free in ∀𝑥𝜑. 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, 12-Oct-2021.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hbnt 2291	Closed theorem version of bound-variable hypothesis builder hbn 2292. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	hbn 2292	If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
Theorem	hbnd 2293	Deduction form of bound-variable hypothesis builder hbn 2292. (Contributed by NM, 3-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓))
Theorem	hbim1 2294	A closed form of hbim 2296. (Contributed by NM, 2-Jun-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	hbimd 2295	Deduction form of bound-variable hypothesis builder hbim 2296. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
Theorem	hbim 2296	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 → 𝜓). (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	hban 2297	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	hb3an 2298	If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	sbi2 2299	Introduction of implication into substitution. (Contributed by NM, 14-May-1993.)
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓))
Theorem	sbim 2300	Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))