P. 33 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexlimdvva 3201*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
Theorem	reximddv2 3202*	Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)
Theorem	r19.29vva 3203*	A commonly used pattern based on r19.29 3103, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	r19.29vvaOLD 3204*	Obsolete version of r19.29vva 3203 as of 4-Nov-2024. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	2rexbiia 3205*	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
Theorem	2ralbidva 3206*	Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	2rexbidva 3207*	Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))
Theorem	2ralbidv 3208*	Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	2rexbidv 3209*	Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rexralbidv 3210*	Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	3ralbidv 3211*	Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜒))
Theorem	4ralbidv 3212*	Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜒))
Theorem	6ralbidv 3213*	Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜒))
Theorem	r19.41vv 3214*	Version of r19.41v 3178 with two quantifiers. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ 𝜓))
Theorem	reeanlem 3215*	Lemma factoring out common proof steps of reeanv 3216 and reean 3303. (Contributed by Wolf Lammen, 20-Aug-2023.)
⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓)))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	reeanv 3216*	Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	3reeanv 3217*	Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒))
Theorem	2ralor 3218*	Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 20-Nov-2024.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓))
Theorem	2ralorOLD 3219*	Obsolete version of 2ralor 3218 as of 20-Nov-2024. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓))
Theorem	risset 3220*	Two ways to say "𝐴 belongs to 𝐵". (Contributed by NM, 22-Nov-1994.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)
Theorem	nelb 3221*	A definition of ¬ 𝐴 ∈ 𝐵. (Contributed by Thierry Arnoux, 20-Nov-2023.) (Proof shortened by SN, 23-Jan-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.)
⊢ (¬ 𝐴 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	nelbOLD 3222*	Obsolete version of nelb 3221 as of 3-Nov-2024. (Contributed by Thierry Arnoux, 20-Nov-2023.) (Proof shortened by SN, 23-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	rspw 3223*	Restricted specialization. Weak version of rsp 3234, requiring ax-8 2100, but not ax-12 2166. (Contributed by GG, 3-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
Theorem	cbvralvw 3224*	Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3347 with a disjoint variable condition, which does not require ax-10 2129, ax-11 2146, ax-12 2166, ax-13 2365. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexvw 3225*	Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3348 with a disjoint variable condition, which does not require ax-10 2129, ax-11 2146, ax-12 2166, ax-13 2365. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvraldva 3226*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Avoid ax-9 2108, ax-ext 2696. (Revised by Wolf Lammen, 9-Mar-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒))
Theorem	cbvrexdva 3227*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Avoid ax-9 2108, ax-ext 2696. (Revised by Wolf Lammen, 9-Mar-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))
Theorem	cbvral2vw 3228*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3351 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2vw 3229*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3352 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	cbvral3vw 3230*	Change bound variables of triple restricted universal quantification, using implicit substitution. Version of cbvral3v 3353 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 10-May-2005.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓)
Theorem	cbvral4vw 3231*	Change bound variables of quadruple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 2-Mar-2025.)
⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 𝜓)
Theorem	cbvral6vw 3232*	Change bound variables of sextuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 5-Mar-2025.)
⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓)
Theorem	cbvral8vw 3233*	Change bound variables of octuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 2-Mar-2025.)
⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑟 = 𝑔 → (𝜎 ↔ 𝜌))    &   ⊢ (𝑠 = ℎ → (𝜌 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐺 ∀ℎ ∈ 𝐻 𝜓)
Theorem	rsp 3234	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
Theorem	rspa 3235	Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑)
Theorem	rspe 3236	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rspec 3237	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 𝜑    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	r19.21bi 3238	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 11-Jun-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
Theorem	r19.21be 3239	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 21-Nov-1994.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
Theorem	r19.21t 3240	Restricted quantifier version of 19.21t 2194; closed form of r19.21 3241. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Wolf Lammen, 2-Jan-2020.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)))
Theorem	r19.21 3241	Restricted quantifier version of 19.21 2195. (Contributed by Scott Fenton, 30-Mar-2011.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	r19.23t 3242	Closed theorem form of r19.23 3243. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)))
Theorem	r19.23 3243	Restricted quantifier version of 19.23 2199. See r19.23v 3172 for a version requiring fewer axioms. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	ralrimi 3244	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). For a version based on fewer axioms see ralrimiv 3134. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3133. (Revised by Wolf Lammen, 4-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralrimia 3245	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexlimi 3246	Restricted quantifier version of exlimi 2205. For a version based on fewer axioms see rexlimiv 3137. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)
Theorem	ralimdaa 3247	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.) (Proof shortened by Wolf Lammen, 29-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	reximdai 3248	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
Theorem	r19.37 3249	Restricted quantifier version of one direction of 19.37 2220. (The other direction does not hold when 𝐴 is empty.) (Contributed by FL, 13-May-2012.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	r19.41 3250	Restricted quantifier version of 19.41 2223. See r19.41v 3178 for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
Theorem	ralrimd 3251	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) For a version based on fewer axioms see ralrimdv 3141. (Contributed by NM, 16-Feb-2004.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexlimd2 3252	Version of rexlimd 3253 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	rexlimd 3253	Deduction form of rexlimd 3253. For a version based on fewer axioms see rexlimdv 3142. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	r19.29af2 3254	A commonly used pattern based on r19.29 3103. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	r19.29af 3255*	A commonly used pattern based on r19.29 3103. See r19.29a 3151, r19.29an 3147 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	reximd2a 3256	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 ∈ 𝐵)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜒)
Theorem	ralbida 3257	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralbidaOLD 3258	Obsolete version of ralbida 3257 as of 31-Oct-2024. (Contributed by NM, 6-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbida 3259	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralbid 3260	Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3167. (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbid 3261	Formula-building rule for restricted existential quantifier (deduction form). For a version based on fewer axioms see rexbidv 3168. (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidvALT 3262*	Alternate proof of rexbidv 3168, shorter but requires more axioms. (Contributed by NM, 20-Nov-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidvaALT 3263*	Alternate proof of rexbidva 3166, shorter but requires more axioms. (Contributed by NM, 9-Mar-1997.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	rsp2 3264	Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	rsp2e 3265	Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof shortened by Wolf Lammen, 7-Jan-2020.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	rspec2 3266	Specialization rule for restricted quantification, with two quantifiers. (Contributed by NM, 20-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)
Theorem	rspec3 3267	Specialization rule for restricted quantification, with three quantifiers. (Contributed by NM, 20-Nov-1994.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)
Theorem	r2alf 3268*	Double restricted universal quantification. For a version based on fewer axioms see r2al 3184. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2allem 3131. (Revised by Wolf Lammen, 9-Jan-2020.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
Theorem	r2exf 3269*	Double restricted existential quantification. For a version based on fewer axioms see r2ex 3185. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2exlem 3132. (Revised by Wolf Lammen, 10-Jan-2020.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))
Theorem	2ralbida 3270*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 24-Feb-2004.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))
Theorem	nfra1 3271	The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑
Theorem	nfre1 3272	The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
Theorem	ralcom4 3273*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralcom4OLD 3274*	Obsolete version of ralcom4 3273 as of 31-Oct-2024. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4 3275*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
Theorem	ralcom 3276*	Commutation of restricted universal quantifiers. See ralcom2 3360 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3360 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom 3277*	Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2024.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexcomOLD 3278*	Obsolete version of rexcom 3277 as of 8-Dec-2024. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4a 3279*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓))
Theorem	ralrot3 3280*	Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑)
Theorem	ralcom13 3281*	Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) (Proof shortened by Wolf Lammen, 2-Jan-2025.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralcom13OLD 3282*	Obsolete version of ralcom13 3281 as of 2-Jan-2025. (Contributed by AV, 3-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom13 3283*	Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexrot4 3284*	Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2ex2rexrot 3285*	Rotate two existential quantifiers and two restricted existential quantifiers. (Contributed by AV, 9-Nov-2023.)
⊢ (∃𝑥∃𝑦∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∃𝑥∃𝑦𝜑)
Theorem	nfra2w 3286*	Similar to Lemma 24 of [Monk2] p. 114, except that quantification is restricted. Once derived from hbra2VD 44441. Version of nfra2 3359 with a disjoint variable condition not requiring ax-13 2365. (Contributed by Alan Sare, 31-Dec-2011.) Reduce axiom usage. (Revised by GG, 24-Sep-2024.) (Proof shortened by Wolf Lammen, 3-Jan-2025.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	nfra2wOLD 3287*	Obsolete version of nfra2w 3286 as of 31-Oct-2024. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by GG, 24-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	hbra1 3288	The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Proof shortened by Wolf Lammen, 7-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralcomf 3289*	Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom 3276. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcomf 3290*	Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom 3277. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	cbvralfw 3291*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 3343 with a disjoint variable condition, which does not require ax-10 2129, ax-13 2365. For a version not dependent on ax-11 2146 and ax-12, see cbvralvw 3224. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2129, ax-13 2365. (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexfw 3292*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3344 with a disjoint variable condition, which does not require ax-13 2365. For a version not dependent on ax-11 2146 and ax-12, see cbvrexvw 3225. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2129, ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralw 3293*	Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3291 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexw 3294*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3292 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	hbral 3295	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
Theorem	nfraldw 3296*	Deduction version of nfralw 3298. Version of nfrald 3355 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 15-Feb-2013.) Avoid ax-9 2108, ax-ext 2696. (Revised by GG, 24-Sep-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexdw 3297*	Deduction version of nfrexw 3300. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2365. See nfrexd 3356 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfralw 3298*	Bound-variable hypothesis builder for restricted quantification. Version of nfral 3357 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 1-Sep-1999.) Avoid ax-13 2365. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 13-Dec-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfralwOLD 3299*	Obsolete version of nfralw 3298 as of 13-Dec-2024. (Contributed by NM, 1-Sep-1999.) (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexw 3300*	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) Add disjoint variable condition to avoid ax-13 2365. See nfrex 3358 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑