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	rexeqbidvv 3301*	Version of rexeqbidv 3315 with additional disjoint variable conditions, not requiring ax-8 2105 nor df-clel 2813. (Contributed by Wolf Lammen, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbi1dv 3302*	Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqbi1dv 3303*	Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	raleq 3304*	Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2134, ax-11 2151, and ax-12 2168. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	rexeq 3305*	Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2134, ax-11 2151, and ax-12 2168. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleqi 3306*	Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)
Theorem	rexeqi 3307*	Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)
Theorem	raleqdv 3308*	Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqdv 3309*	Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	raleqbii 3310	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)
Theorem	rexeqbii 3311	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)
Theorem	raleleq 3312*	All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleleqALT 3313*	Alternate proof of raleleq 3312 using ralel 3063, being longer and using more axioms. (Contributed by AV, 30-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	raleqbidv 3314*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2134, ax-11 2151, and ax-12 2168 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidv 3315*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2134, ax-11 2151, and ax-12 2168 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbidva 3316*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidva 3317*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	cbvraldva2 3318*	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 3319*	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 3320*	Obsolete version of cbvrexdva2 3319 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	cbvraldva 3321*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒))
Theorem	cbvrexdva 3322*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))
Theorem	raleqf 3323	Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See raleq 3304 for a version based on fewer axioms. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	rexeqf 3324	Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See rexeq 3305 for a version based on fewer axioms. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))
Theorem	raleqbid 3325	Equality deduction for restricted universal quantifier. See raleqbidv 3314 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbid 3326	Equality deduction for restricted existential quantifier. See rexeqbidv 3315 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	sbralie 3327*	Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	rgen2a 3328*	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2448. This theorem relies on the full set of axioms up to ax-ext 2706 and it should no longer be used. Usage of rgen2 3189 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 3329	Deduction version of nfral 3331. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker nfraldw 3287 when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓)
Theorem	nfrexd 3330	Deduction version of nfrex 3332. Usage of this theorem is discouraged because it depends on ax-13 2369. See nfrexdw 3288 for a version with a disjoint variable condition, but not requiring ax-13 2369. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓)
Theorem	nfral 3331	Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker nfralw 3289 when possible. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑
Theorem	nfrex 3332	Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2369. See nfrexw 3291 for a version with a disjoint variable condition, but not requiring ax-13 2369. (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 3333*	Similar to Lemma 24 of [Monk2] p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD 42706. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker nfra2w 3277 when possible. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	ralcom2 3334*	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 2706 and it should no longer be used. Usage of ralcom 3267 is highly encouraged. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑)
Theorem	cbvralf 3335	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbvralfw 3282 when possible. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexf 3336	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbvrexfw 3283 when possible. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Syntax	wreu 3337	Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥 ∈ 𝐴 𝜑
Syntax	wrmo 3338	Extend wff notation to include restricted "at most one".
wff ∃*𝑥 ∈ 𝐴 𝜑
Definition	df-rmo 3339	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 3061). (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-reu 3340	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 3061). (Contributed by NM, 22-Nov-1994.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	reu5 3341	Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	reurmo 3342	Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reurex 3343	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	mormo 3344	Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmoanid 3345	Cancellation law for restricted at-most-one quantification. (Contributed by Peter Mazsa, 24-May-2018.)
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reuanid 3346	Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.)
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	rmobiia 3347	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓)
Theorem	reubiia 3348	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	rmobii 3349	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓)
Theorem	reubii 3350	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)
Theorem	2reu2rex 3351	Double restricted existential uniqueness, analogous to 2eu2ex 2642. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	rmobidva 3352*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) Avoid ax-6 1968, ax-7 2008, ax-12 2168. (Revised by Wolf Lammen, 23-Nov-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubidva 3353*	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 3354*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reubidv 3355*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Syntax	crab 3356	Extend class notation to include the restricted class abstraction (class builder).
class {𝑥 ∈ 𝐴 ∣ 𝜑}
Definition	df-rab 3357	Define a restricted class abstraction (class builder): {𝑥 ∈ 𝐴 ∣ 𝜑} is the class of all sets 𝑥 in 𝐴 such that 𝜑(𝑥) is true. Definition of [TakeutiZaring] p. 20. For the interpretation given in the previous paragraph to be correct, we need to assume Ⅎ𝑥𝐴, which is the case as soon as 𝑥 and 𝐴 are disjoint, which is generally the case. If 𝐴 were to depend on 𝑥, then the interpretation would be less obvious (think of the two extreme cases 𝐴 = {𝑥} and 𝐴 = 𝑥, for instance). See also df-ral 3061. (Contributed by NM, 22-Nov-1994.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	nfreu1 3358	The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.)
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑
Theorem	nfrmo1 3359	The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.)
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑
Theorem	nfreud 3360	Deduction version of nfreu 3366. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmod 3361	Deduction version of nfrmo 3367. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by NM, 17-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓)
Theorem	nfrmow 3362*	Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3367 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2113, ax-ext 2706. (Revised by Wolf Lammen, 21-Nov-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	nfreuw 3363*	Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3366 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 30-Oct-2010.) (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2113, ax-ext 2706. (Revised by Wolf Lammen, 21-Nov-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑
Theorem	nfreuwOLD 3364*	Obsolete version of nfreuw 3363 as of 21-Nov-2024. (Contributed by NM, 30-Oct-2010.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑
Theorem	nfrmowOLD 3365*	Obsolete version of nfrmow 3362 as of 21-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	nfreu 3366	Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker nfreuw 3363 when possible. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑
Theorem	nfrmo 3367	Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker nfrmow 3362 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑
Theorem	rabid 3368	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	rabrab 3369	Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.)
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	rabidim1 3370	Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴)
Theorem	rabid2f 3371	An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rabid2 3372*	An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2024.)
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rabid2OLD 3373*	Obsolete version of rabid2 3372 as of 24-11-2024. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rabbi 3374	Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3419. (Contributed by NM, 25-Nov-2013.)
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	nfrab1 3375	The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}
Theorem	nfrabw 3376*	A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3378 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	nfrabwOLD 3377*	Obsolete version of nfrabw 3376 as of 23-Nov2024. (Contributed by NM, 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	nfrab 3378	A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker nfrabw 3376 when possible. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}
Theorem	reubida 3379	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))
Theorem	rmobida 3380	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	rmobidvaOLD 3381*	Obsolete version of rmobidv 3354 as of 23-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒))
Theorem	reueq1f 3382	Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑))
Theorem	rmoeq1f 3383	Equality theorem for restricted at-most-one quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	reueq1 3384*	Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2134, ax-11 2151, and ax-12 2168. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑))
Theorem	rmoeq1 3385*	Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2134, ax-11 2151, and ax-12 2168. (Revised by Steven Nguyen, 30-Apr-2023.)
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	reueqd 3386*	Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqd 3387*	Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	moel 3388*	"At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) Avoid ax-11 2151. (Revised by Wolf Lammen, 23-Nov-2024.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦)
Theorem	moelOLD 3389*	Obsolete version of moel 3388 as of 23-Nov-2024. (Contributed by Thierry Arnoux, 26-Jul-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦)
Theorem	rmo5 3390	Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	nrexrmo 3391	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reueubd 3392*	Restricted existential uniqueness is equivalent to existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝑉 𝜓 ↔ ∃!𝑥𝜓))
Theorem	cbvrmow 3393*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3400 with a disjoint variable condition, which does not require ax-10 2134, ax-13 2369. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 23-May-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuw 3394*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3399 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2134. (Revised by Wolf Lammen, 10-Dec-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuwOLD 3395*	Obsolete version of cbvreuw 3394 as of 10-Dec-2024. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmowOLD 3396*	Obsolete version of cbvrmow 3393 as of 23-May-2024. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvral 3397*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbvralw 3284 when possible. (Contributed by NM, 31-Jul-2003.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrex 3398*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbvrexw 3285 when possible. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreu 3399*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbvreuw 3394 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmo 3400*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbvrmow 3393, cbvrmovw 3401 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)