P. 34 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3301-3400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfra2w 3301*	Similar to Lemma 24 of [Monk2] p. 114, except that quantification is restricted. Once derived from hbra2VD 45433. Version of nfra2 3366 with a disjoint variable condition not requiring ax-13 2406. (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	hbra1 3302	The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Proof shortened by Wolf Lammen, 7-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥∀𝑥 ∈ 𝐴 𝜑)
Theorem	ralcomf 3303*	Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom 3293. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcomf 3304*	Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom 3294. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	cbvralfw 3305*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 3350 with a disjoint variable condition, which does not require ax-10 2178, ax-13 2406. For a version not dependent on ax-11 2194 and ax-12, see cbvralvw 3243. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2178, ax-13 2406. (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexfw 3306*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3351 with a disjoint variable condition, which does not require ax-13 2406. For a version not dependent on ax-11 2194 and ax-12, see cbvrexvw 3244. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2178, ax-13 2406. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralw 3307*	Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3305 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexw 3308*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3306 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	hbral 3309	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
Theorem	nfraldw 3310*	Deduction version of nfralw 3312. Version of nfrald 3362 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 15-Feb-2013.) Avoid ax-9 2155, ax-ext 2737. (Revised by GG, 24-Sep-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexdw 3311*	Deduction version of nfrexw 3313. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2406. See nfrexd 3363 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfralw 3312*	Bound-variable hypothesis builder for restricted quantification. Version of nfral 3364 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 1-Sep-1999.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 13-Dec-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexw 3313*	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 2406. See nfrex 3365 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	r19.12 3314*	Restricted quantifier version of 19.12 2362. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2406, ax-ext 2737. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	reean 3315*	Rearrange restricted existential quantifiers. For a version based on fewer axioms see reeanv 3237. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	cbvralsvw 3316*	Change bound variable by using a substitution. Version of cbvralsv 3356 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) Avoid ax-10 2178, ax-12 2215. (Revised by SN, 21-Aug-2025.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvrexsvw 3317*	Change bound variable by using a substitution. Version of cbvrexsv 3357 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 2-Mar-2008.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvralsvwOLD 3318*	Obsolete version of cbvralsvw 3316 as of 21-Aug-2025. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	rexeq 3319*	Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleq 3320*	Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	raleqi 3321*	Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)
Theorem	rexeqi 3322*	Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)
Theorem	raleqdv 3323*	Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqdv 3324*	Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	raleqtrdv 3325*	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexeqtrdv 3326*	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	raleqtrrdv 3327*	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐵 = 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexeqtrrdv 3328*	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐵 = 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	raleqbidva 3329*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidva 3330*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbidvv 3331*	Version of raleqbidv 3339 with additional disjoint variable conditions, not requiring ax-8 2147 nor df-clel 2840. (Contributed by BJ, 22-Sep-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidvv 3332*	Version of rexeqbidv 3340 with additional disjoint variable conditions, not requiring ax-8 2147 nor df-clel 2840. (Contributed by Wolf Lammen, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbi1dv 3333*	Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqbi1dv 3334*	Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	raleleq 3335*	All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.) (Proof shortened by Wolf Lammen, 18-Jul-2025.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleleqOLD 3336*	Obsolete version of raleleq 3335 as of 18-Jul-2025. (Contributed by AV, 30-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleqbii 3337	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)
Theorem	rexeqbii 3338	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)
Theorem	raleqbidv 3339*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidv 3340*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	cbvraldva2 3341*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
Theorem	cbvrexdva2 3342*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 8-Jan-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	sbralie 3343*	Implicit to explicit substitution that swaps variables in a restrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004.) Avoid ax-ext 2737, df-cleq 2757, df-clel 2840. (Revised by Wolf Lammen, 10-Mar-2025.) Avoid ax-10 2178, ax-12 2215. (Revised by SN, 13-Nov-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	sbralieALT 3344*	Alternative shorter proof of sbralie 3343 dependent on ax-ext 2737, df-cleq 2757, df-clel 2840. (Contributed by NM, 5-Sep-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	sbralieOLD 3345*	Obsolete version of sbralie 3343 as of 13-Nov-2025. (Contributed by NM, 5-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	raleqf 3346	Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See raleq 3320 for a version based on fewer axioms. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	rexeqf 3347	Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See rexeq 3319 for a version based on fewer axioms. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 9-Mar-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleqbid 3348	Equality deduction for restricted universal quantifier. See raleqbidv 3339 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbid 3349	Equality deduction for restricted existential quantifier. See rexeqbidv 3340 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	cbvralf 3350	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvralfw 3305 when possible. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexf 3351	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrexfw 3306 when possible. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvral 3352*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvralw 3307 when possible. (Contributed by NM, 31-Jul-2003.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrex 3353*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrexw 3308 when possible. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralv 3354*	Change the bound variable of a restricted universal quantifier using implicit substitution. See cbvralvw 3243 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvralvw 3243 when possible. (Contributed by NM, 28-Jan-1997.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexv 3355*	Change the bound variable of a restricted existential quantifier using implicit substitution. See cbvrexvw 3244 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrexvw 3244 when possible. (Contributed by NM, 2-Jun-1998.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralsv 3356*	Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvralsvw 3316 when possible. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvrexsv 3357*	Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrexsvw 3317 when possible. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvral2v 3358*	Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvral2vw 3247 when possible. (Contributed by NM, 10-Aug-2004.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2v 3359*	Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvrex2vw 3248 when possible. (Contributed by FL, 2-Jul-2012.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	cbvral3v 3360*	Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvral3vw 3249 when possible. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓)
Theorem	rgen2a 3361*	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2485. This theorem relies on the full set of axioms up to ax-ext 2737 and it should no longer be used. Usage of rgen2 3205 is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrald 3362	Deduction version of nfral 3364. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfraldw 3310 when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexd 3363	Deduction version of nfrex 3365. Usage of this theorem is discouraged because it depends on ax-13 2406. See nfrexdw 3311 for a version with a disjoint variable condition, but not requiring ax-13 2406. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfral 3364	Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfralw 3312 when possible. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrex 3365	Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2406. See nfrexw 3313 for a version with a disjoint variable condition, but not requiring ax-13 2406. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	nfra2 3366*	Similar to Lemma 24 of [Monk2] p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD 45433. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfra2w 3301 when possible. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	ralcom2 3367*	Commutation of restricted universal quantifiers. Note that 𝑥 and 𝑦 need not be disjoint (this makes the proof longer). This theorem relies on the full set of axioms up to ax-ext 2737 and it should no longer be used. Usage of ralcom 3293 is highly encouraged. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑)
2.1.5.2  Restricted existential uniqueness and at-most-one quantifier
Syntax	wreu 3368	Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥 ∈ 𝐴 𝜑
Syntax	wrmo 3369	Extend wff notation to include restricted "at most one".
wff ∃*𝑥 ∈ 𝐴 𝜑
Definition	df-rmo 3370	Define restricted "at most one". Note: This notation is most often used to express that 𝜑 holds for at most one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3080). (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-reu 3371	Define restricted existential uniqueness. Note: This notation is most often used to express that 𝜑 holds for exactly one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3080). (Contributed by NM, 22-Nov-1994.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	reu5 3372	Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	reurmo 3373	Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reurex 3374	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	mormo 3375	Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmobiia 3376	Formula-building rule for restricted at-most-one quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓)
Theorem	reubiia 3377	Formula-building rule for restricted existential uniqueness quantifier (inference form). (Contributed by NM, 14-Nov-2004.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	rmobii 3378	Formula-building rule for restricted at-most-one quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓)
Theorem	reubii 3379	Formula-building rule for restricted existential uniqueness quantifier (inference form). (Contributed by NM, 22-Oct-1999.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	rmoanid 3380	Cancellation law for restricted at-most-one quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reuanid 3381	Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	2reu2rex 3382	Double restricted existential uniqueness, analogous to 2eu2ex 2673. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	rmobidva 3383*	Formula-building rule for restricted at-most-one quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) Avoid ax-12 2215. (Revised by Wolf Lammen, 23-Nov-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubidva 3384*	Formula-building rule for restricted existential uniqueness quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Theorem	rmobidv 3385*	Formula-building rule for restricted at-most-one quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubidv 3386*	Formula-building rule for restricted existential uniqueness quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Theorem	reueubd 3387*	Restricted existential uniqueness is equivalent to existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝑉 𝜓 ↔ ∃!𝑥𝜓))
Theorem	rmo5 3388	Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	nrexrmo 3389	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	moel 3390*	"At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) Avoid ax-11 2194. (Revised by Wolf Lammen, 23-Nov-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦)
Theorem	cbvrmovw 3391*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmov 3411 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 16-Jun-2017.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuvw 3392*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreuv 3412 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 5-Apr-2004.) (Revised by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	rmobida 3393	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubida 3394	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Theorem	cbvrmow 3395*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3410 with a disjoint variable condition, which does not require ax-10 2178, ax-13 2406. (Contributed by NM, 16-Jun-2017.) Avoid ax-10 2178, ax-13 2406. (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuw 3396*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3409 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2178. (Revised by Wolf Lammen, 10-Dec-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmo1 3397	The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.)
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑
Theorem	nfreu1 3398	The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.)
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑
Theorem	nfrmow 3399*	Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3415 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 16-Jun-2017.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) Avoid ax-9 2155, ax-ext 2737. (Revised by Wolf Lammen, 21-Nov-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	nfreuw 3400*	Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3416 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 30-Oct-2010.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) Avoid ax-9 2155, ax-ext 2737. (Revised by Wolf Lammen, 21-Nov-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑