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	rexcomf 3301*	Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom 3288. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	cbvralfw 3302*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 3357 with a disjoint variable condition, which does not require ax-10 2138, ax-13 2372. For a version not dependent on ax-11 2155 and ax-12, see cbvralvw 3235. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2138, ax-13 2372. (Revised by Gino Giotto, 23-May-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexfw 3303*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3358 with a disjoint variable condition, which does not require ax-13 2372. For a version not dependent on ax-11 2155 and ax-12, see cbvrexvw 3236. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2138, ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralw 3304*	Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3302 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexw 3305*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 3303 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	hbral 3306	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦 ∈ 𝐴 𝜑 → ∀𝑥∀𝑦 ∈ 𝐴 𝜑)
Theorem	nfraldw 3307*	Deduction version of nfralw 3309. Version of nfrald 3369 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 15-Feb-2013.) Avoid ax-9 2117, ax-ext 2704. (Revised by Gino Giotto, 24-Sep-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexdw 3308*	Deduction version of nfrexw 3311. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2372. See nfrexd 3370 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfralw 3309*	Bound-variable hypothesis builder for restricted quantification. Version of nfral 3371 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 1-Sep-1999.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 13-Dec-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfralwOLD 3310*	Obsolete version of nfralw 3309 as of 13-Dec-2024. (Contributed by NM, 1-Sep-1999.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrexw 3311*	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 2372. See nfrex 3372 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑
Theorem	r19.12 3312*	Restricted quantifier version of 19.12 2321. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2372, ax-ext 2704. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	r19.12OLD 3313*	Obsolete version of 19.12 2321 as of 4-Nov-2024. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2372, ax-ext 2704. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
Theorem	reean 3314*	Rearrange restricted existential quantifiers. For a version based on fewer axioms see reeanv 3227. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	cbvralsvw 3315*	Change bound variable by using a substitution. Version of cbvralsv 3363 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvrexsvw 3316*	Change bound variable by using a substitution. Version of cbvrexsv 3364 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 2-Mar-2008.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvralsvwOLD 3317*	Obsolete version of cbvralsvw 3315 as of 8-Mar-2025. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvrexsvwOLD 3318*	Obsolete version of cbvrexsvw 3316 as of 8-Mar-2025. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	nfraldwOLD 3319*	Obsolete version of nfraldw 3307 as of 24-Sep-2024. (Contributed by NM, 15-Feb-2013.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfra2wOLDOLD 3320*	Obsolete version of nfra2w 3297 as of 24-Sep-2024. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	cbvralfwOLD 3321*	Obsolete version of cbvralfw 3302 as of 23-May-2024. (Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	rexeq 3322*	Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleq 3323*	Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.)
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	raleqi 3324*	Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)
Theorem	rexeqi 3325*	Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)
Theorem	raleqdv 3326*	Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqdv 3327*	Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	raleqbidva 3328*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidva 3329*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbidvv 3330*	Version of raleqbidv 3343 with additional disjoint variable conditions, not requiring ax-8 2109 nor df-clel 2811. (Contributed by BJ, 22-Sep-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbidvvOLD 3331*	Version of raleqbidv 3343 with additional disjoint variable conditions, not requiring ax-8 2109 nor df-clel 2811. (Contributed by BJ, 22-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidvv 3332*	Version of rexeqbidv 3344 with additional disjoint variable conditions, not requiring ax-8 2109 nor df-clel 2811. (Contributed by Wolf Lammen, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidvvOLD 3333*	Version of rexeqbidv 3344 with additional disjoint variable conditions, not requiring ax-8 2109 nor df-clel 2811. (Contributed by Wolf Lammen, 25-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbi1dv 3334*	Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqbi1dv 3335*	Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	raleqOLD 3336*	Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	rexeqOLD 3337*	Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleleq 3338*	All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.) Avoid ax-8 2109. (Revised by Wolf Lammen, 9-Mar-2025.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleqbii 3339	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)
Theorem	rexeqbii 3340	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)
Theorem	raleleqOLD 3341*	Obsolete version of raleleq 3338 as of 9-Mar-2025. (Contributed by AV, 30-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleleqALT 3342*	Alternate proof of raleleq 3338 using ralel 3065, being longer and using more axioms. (Contributed by AV, 30-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleqbidv 3343*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidv 3344*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	cbvraldva2 3345*	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 3346*	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	cbvrexdva2OLD 3347*	Obsolete version of cbvrexdva2 3346 as of 8-Jan-2025. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 12-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	cbvraldvaOLD 3348*	Obsolete version of cbvraldva 3237 as of 9-Mar-2025. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒))
Theorem	cbvrexdvaOLD 3349*	Obsolete version of cbvrexdva 3238 as of 9-Mar-2025. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))
Theorem	raleqf 3350	Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See raleq 3323 for a version based on fewer axioms. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	rexeqf 3351	Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See rexeq 3322 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	rexeqfOLD 3352	Obsolete version of rexeqf 3351 as of 9-Mar-2025. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleqbid 3353	Equality deduction for restricted universal quantifier. See raleqbidv 3343 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbid 3354	Equality deduction for restricted existential quantifier. See rexeqbidv 3344 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	sbralie 3355*	Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004.) Avoid ax-ext 2704. (Revised by Wolf Lammen, 10-Mar-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	sbralieALT 3356*	Alternative shorter proof of sbralie 3355 dependent on ax-ext 2704. (Contributed by NM, 5-Sep-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	cbvralf 3357	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvralfw 3302 when possible. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexf 3358	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvrexfw 3303 when possible. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvral 3359*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvralw 3304 when possible. (Contributed by NM, 31-Jul-2003.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrex 3360*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvrexw 3305 when possible. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralv 3361*	Change the bound variable of a restricted universal quantifier using implicit substitution. See cbvralvw 3235 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvralvw 3235 when possible. (Contributed by NM, 28-Jan-1997.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexv 3362*	Change the bound variable of a restricted existential quantifier using implicit substitution. See cbvrexvw 3236 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvrexvw 3236 when possible. (Contributed by NM, 2-Jun-1998.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralsv 3363*	Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvralsvw 3315 when possible. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvrexsv 3364*	Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvrexsvw 3316 when possible. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvral2v 3365*	Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvral2vw 3239 when possible. (Contributed by NM, 10-Aug-2004.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2v 3366*	Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvrex2vw 3240 when possible. (Contributed by FL, 2-Jul-2012.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	cbvral3v 3367*	Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvral3vw 3241 when possible. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓)
Theorem	rgen2a 3368*	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2451. This theorem relies on the full set of axioms up to ax-ext 2704 and it should no longer be used. Usage of rgen2 3198 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 3369	Deduction version of nfral 3371. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfraldw 3307 when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexd 3370	Deduction version of nfrex 3372. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfrexdw 3308 for a version with a disjoint variable condition, but not requiring ax-13 2372. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfral 3371	Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfralw 3309 when possible. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrex 3372	Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfrexw 3311 for a version with a disjoint variable condition, but not requiring ax-13 2372. (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 3373*	Similar to Lemma 24 of [Monk2] p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD 43621. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfra2w 3297 when possible. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	ralcom2 3374*	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 2704 and it should no longer be used. Usage of ralcom 3287 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 3375	Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥 ∈ 𝐴 𝜑
Syntax	wrmo 3376	Extend wff notation to include restricted "at most one".
wff ∃*𝑥 ∈ 𝐴 𝜑
Definition	df-rmo 3377	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 3063). (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-reu 3378	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 3063). (Contributed by NM, 22-Nov-1994.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	reu5 3379	Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	reurmo 3380	Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reurex 3381	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	mormo 3382	Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmobiia 3383	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓)
Theorem	reubiia 3384	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	rmobii 3385	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓)
Theorem	reubii 3386	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	rmoanid 3387	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 3388	Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	rmoanidOLD 3389	Obsolete version of rmoanid 3387 as of 12-Jan-2025. (Contributed by Peter Mazsa, 24-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reuanidOLD 3390	Obsolete version of reuanid 3388 as of 12-Jan-2025. (Contributed by Peter Mazsa, 12-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	2reu2rex 3391	Double restricted existential uniqueness, analogous to 2eu2ex 2640. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	rmobidva 3392*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) Avoid ax-6 1972, ax-7 2012, ax-12 2172. (Revised by Wolf Lammen, 23-Nov-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubidva 3393*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Theorem	rmobidv 3394*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubidv 3395*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Theorem	reueubd 3396*	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 3397	Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	nrexrmo 3398	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	moel 3399*	"At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) Avoid ax-11 2155. (Revised by Wolf Lammen, 23-Nov-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦)
Theorem	cbvrmovw 3400*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmov 3427 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)