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	hbald 2201	Deduction form of bound-variable hypothesis builder hbal 2200. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓))
Theorem	sbal 2202*	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 2203*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥]∀𝑧𝜑 ↔ ∀𝑧𝜓)
Theorem	hbsbw 2204*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Version of hbsb 2554 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 2205*	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 2206*	Obsolete version of sbco4lem 2134 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 2207*	Obsolete version of sbco4 2135 as of 3-Sep-2025. (Contributed by Jim Kingdon, 25-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑢][𝑥 / 𝑣][𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	nfa2 2208	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) Remove dependency on ax-12 2211. (Revised by Wolf Lammen, 18-Oct-2021.)
⊢ Ⅎ𝑥∀𝑦∀𝑥𝜑
Theorem	nfexhe 2209	Version of nfex 2355 with the existential dual to the 'h' hypothesis, avoiding ax-12 2211. (Contributed by SN, 11-Feb-2026.)
⊢ (∃𝑥𝜑 → 𝜑)    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	nfexa2 2210	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 2211	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 2117). 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 39631 and was replaced with this shorter ax-12 2211 in Jan. 2007. The old axiom is proved from this one as Theorem axc15 2452. Conversely, this axiom is proved from ax-c15 39631 as Theorem ax12 2453. Juha Arpiainen proved the metalogical independence of this axiom (in the form of the older axiom ax-c15 39631) from the others on 19-Jan-2006. See item 9a at https://us.metamath.org/award2003.html 39631. See ax12v 2212 and ax12v2 2213 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions. This axiom scheme is logically redundant (see ax12w 2166) but is used as an auxiliary axiom scheme to achieve scheme completeness. (Contributed by NM, 22-Jan-2007.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12v 2212*	This is essentially Axiom ax-12 2211 weakened by additional restrictions on variables. Besides axc11r 2398, this theorem should be the only one referencing ax-12 2211 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 1938, 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 2213*	It is possible to remove any restriction on 𝜑 in ax12v 2212. Same as Axiom C8 of [Monk2] p. 105. Use ax12v 2212 instead when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-10 2174 and ax-13 2402. (Revised by Jim Kingdon, 15-Dec-2017.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12ev2 2214*	Version of ax12v2 2213 rewritten to use an existential quantifier. One direction of sbalex 2276 without the universal quantifier, avoiding ax-10 2174. (Contributed by SN, 14-Aug-2025.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → (𝑥 = 𝑦 → 𝜑))
Theorem	19.8a 2215	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 2011 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 2217. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	19.8ad 2216	If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2215. (Contributed by DAW, 13-Feb-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	sp 2217	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 2100. This theorem shows that our obsolete axiom ax-c5 39625 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 2211. It is thought the best we can do using only Tarski's axioms is spw 2062. Also see spvw 2009 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 2218	Inference rule of universal instantiation, or universal specialization. Converse of the inference rule of (universal) generalization ax-gen 1823. Contrary to the rule of generalization, its closed form is valid, see sp 2217. (Contributed by NM, 5-Aug-1993.)
⊢ ∀𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	sps 2219	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	2sp 2220	A double specialization (see sp 2217). Another double specialization, closer to PM*11.1, is 2stdpc4 2102. (Contributed by BJ, 15-Sep-2018.)
⊢ (∀𝑥∀𝑦𝜑 → 𝜑)
Theorem	spsd 2221	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	19.2g 2222	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. Use 19.2 2004 when sufficient. (Contributed by Mel L. O'Cat, 31-Mar-2008.)
⊢ (∀𝑥𝜑 → ∃𝑦𝜑)
Theorem	19.21bi 2223	Inference form of 19.21 2241 and also deduction form of sp 2217. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.21bbi 2224	Inference removing two universal quantifiers. Version of 19.21bi 2223 with two quantifiers. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → ∀𝑥∀𝑦𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.23bi 2225	Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2245. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	nexr 2226	Inference associated with the contrapositive of 19.8a 2215. (Contributed by Jeff Hankins, 26-Jul-2009.)
⊢ ¬ ∃𝑥𝜑    ⇒   ⊢ ¬ 𝜑
Theorem	qexmid 2227	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 2228	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) df-nf 1812 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 23-Nov-2023.)
⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	nf5ri 2229	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nf5rd 2230	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	spimedv 2231*	Deduction version of spimev 2422. Version of spimed 2418 with a disjoint variable condition, which does not require ax-13 2402. See spime 2419 for a non-deduction version. (Contributed by NM, 14-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝜒 → Ⅎ𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓))
Theorem	spimefv 2232*	Version of spime 2419 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	nfim1 2233	A closed form of nfim 1924. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1812 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfan1 2234	A closed form of nfan 1927. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1812 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	19.3t 2235	Closed form of 19.3 2236 and version of 19.9t 2238 with a universal quantifier. (Contributed by NM, 9-Nov-2020.) (Proof shortened by BJ, 9-Oct-2022.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥𝜑 ↔ 𝜑))
Theorem	19.3 2236	A wff may be quantified with a variable not free in it. Version of 19.9 2239 with a universal quantifier. Theorem 19.3 of [Margaris] p. 89. See 19.3v 2010 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.9d 2237	A deduction version of one direction of 19.9 2239. (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 1812 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
⊢ (𝜓 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	19.9t 2238	Closed form of 19.9 2239 and version of 19.3t 2235 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 2239	A wff may be existentially quantified with a variable not free in it. Version of 19.3 2236 with an existential quantifier. Theorem 19.9 of [Margaris] p. 89. See 19.9v 2012 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 2240	Closed form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2241. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) df-nf 1812 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 3-Nov-2021.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21 2241	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See 19.21v 1967 for a version requiring fewer axioms. See also 19.21h 2320. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) df-nf 1812 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	stdpc5 2242	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 2041. 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 1966 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 2174. (Revised by Wolf Lammen, 4-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	19.21-2 2243	Version of 19.21 2241 with two quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	19.23t 2244	Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23 2245. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) df-nf 1812 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	19.23 2245	Theorem 19.23 of [Margaris] p. 90. See 19.23v 1970 for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	alimd 2246	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1838. See alimdh 1845, alimdv 1944 for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alrimi 2247	Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2241. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	alrimdd 2248	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2241. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 2249	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2241. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximd 2250	Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1862. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	exlimi 2251	Inference associated with 19.23 2245. See exlimiv 1958 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 2252	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 2253	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2254. (Revised by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exlimdd 2254	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	nexd 2255	Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	albid 2256	Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbid 2257	Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	nfbidf 2258	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1812 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒))
Theorem	19.16 2259	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓))
Theorem	19.17 2260	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓))
Theorem	19.27 2261	Theorem 19.27 of [Margaris] p. 90. See 19.27v 2023 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28 2262	Theorem 19.28 of [Margaris] p. 90. See 19.28v 2024 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 7-May-2025.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.19 2263	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓))
Theorem	19.36 2264	Theorem 19.36 of [Margaris] p. 90. See 19.36v 2021 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓))
Theorem	19.36i 2265	Inference associated with 19.36 2264. See 19.36iv 1974 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.37 2266	Theorem 19.37 of [Margaris] p. 90. See 19.37v 2025 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.32 2267	Theorem 19.32 of [Margaris] p. 90. See 19.32v 1968 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓))
Theorem	19.31 2268	Theorem 19.31 of [Margaris] p. 90. See 19.31v 1969 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓))
Theorem	19.41 2269	Theorem 19.41 of [Margaris] p. 90. See 19.41v 1977 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 2270	Theorem 19.42 of [Margaris] p. 90. See 19.42v 1981 for a version requiring fewer axioms. See exan 1890 for an immediate version. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	19.44 2271	Theorem 19.44 of [Margaris] p. 90. See 19.44v 2026 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45 2272	Theorem 19.45 of [Margaris] p. 90. See 19.45v 2027 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	spimfv 2273*	Specialization, using implicit substitution. Version of spim 2417 with a disjoint variable condition, which does not require ax-13 2402. See spimvw 2014 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2420 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarfv 2274*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2425 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	cbv3v2 2275*	Version of cbv3 2427 with two disjoint variable conditions, which does not require ax-11 2190 nor ax-13 2402. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	sbalex 2276*	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 2095. That both sides of the biconditional express proper substitution is proved by sb5 2309 and sb6 2117. The implication "to the left" is equs4v 2028 and does not require ax-10 2174 nor ax-12 2211. It also holds without disjoint variable condition if we allow more axioms (see equs4 2446). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2490 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2489 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2302 in place of equsex 2448 in order to remove dependency on ax-13 2402. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2095. (Revised by BJ, 21-Sep-2024.) (Proof shortened by SN, 14-Aug-2025.)
⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbalexOLD 2277*	Obsolete version of sbalex 2276 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 2278*	Version of sb4a 2510 with a disjoint variable condition, which does not require ax-13 2402. The distinctor antecedent from sb4b 2505 is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	sbimd 2279	Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2095. (Revised by Steven Nguyen, 9-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒))
Theorem	sbbid 2280	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2174 and ax-13 2402. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2095. (Revised by Steven Nguyen, 11-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	2sbbid 2281	Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒))
Theorem	sbequ1 2282	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2095. (Revised by BJ, 22-Dec-2020.)
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑))
Theorem	sbequ2 2283	An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2095. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.)
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑))
Theorem	stdpc7 2284	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2056.) 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 2285	An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Theorem	sbequ12r 2286	An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑))
Theorem	sbelx 2287*	Elimination of substitution. Also see sbel2x 2504. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2402. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2174. (Revised by GG, 20-Aug-2023.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbequ12a 2288	An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.)
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑))
Theorem	sbid 2289	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 2290*	A composition law for substitution. Version of sbco 2537 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 2291*	Obsolete version of sbcov 2290 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 2292*	Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	sbid2vw 2293*	Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2539, at the expense of an extra distinct variable condition. (Contributed by NM, 14-May-1993.) (Revised by Wolf Lammen, 5-Aug-2023.)
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑)
Theorem	axc16g 2294*	Generalization of axc16 2295. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2036 }, Theorem ax12v 2212. (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 2402, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2299. (Revised by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	axc16 2295*	Proof of older axiom ax-c16 39634. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gb 2296*	Biconditional strengthening of axc16g 2294. (Contributed by NM, 15-May-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑))
Theorem	axc16nf 2297*	If dtru 5418 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 2190. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2174. (Revised by Wolf Lammen, 12-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	axc11v 2298*	Version of axc11 2460 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2036 }, from ax12v 2212 (contrary to axc11 2460 which seems to require the full ax-12 2211 and ax-13 2402). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	axc11rv 2299*	Version of axc11r 2398 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2036 }, from ax12v 2212 (contrary to axc11 2460 which seems to require the full ax-12 2211 and ax-13 2402, and to axc11r 2398 which seems to require the full ax-12 2211). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑))
Theorem	drsb2 2300	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.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))