P. 28 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2701-2800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	raleqtrdv 2701*	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexeqtrdv 2702*	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	raleqtrrdv 2703*	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐵 = 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexeqtrrdv 2704*	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐵 = 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	raleqbi1dv 2705*	Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	rexeqbi1dv 2706*	Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))
Theorem	reueqd 2707*	Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqd 2708*	Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	raleqbidv 2709*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidv 2710*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	raleqbidva 2711*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
Theorem	rexeqbidva 2712*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
Theorem	mormo 2713	Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	reu5 2714	Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
Theorem	reurex 2715	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)
Theorem	reurmo 2716	Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	rmo5 2717	Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	nrexrmo 2718	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)
Theorem	cbvralfw 2719*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 2721 with a disjoint variable condition. Although we don't do so yet, we expect this disjoint variable condition will allow us to remove reliance on ax-i12 1521 and ax-bndl 1523 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexfw 2720*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2722 with a disjoint variable condition. Although we don't do so yet, we expect this disjoint variable condition will allow us to remove reliance on ax-i12 1521 and ax-bndl 1523 in the proof. (Contributed by FL, 27-Apr-2008.) (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralf 2721	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexf 2722	Rule used to change bound variables, using implicit substitution. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) (Proof rewritten by Jim Kingdon, 10-Jun-2018.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralw 2723*	Rule used to change bound variables, using implicit substitution. Version of cbvral 2725 with a disjoint variable condition. Although we don't do so yet, we expect this disjoint variable condition will allow us to remove reliance on ax-i12 1521 and ax-bndl 1523 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexw 2724*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2720 with more disjoint variable conditions. Although we don't do so yet, we expect the disjoint variable conditions will allow us to remove reliance on ax-i12 1521 and ax-bndl 1523 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvral 2725*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrex 2726*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreu 2727*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmo 2728*	Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralv 2729*	Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexv 2730*	Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuv 2731*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrmov 2732*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓)
Theorem	cbvralvw 2733*	Version of cbvralv 2729 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
Theorem	cbvrexvw 2734*	Version of cbvrexv 2730 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
Theorem	cbvreuvw 2735*	Version of cbvreuv 2731 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
Theorem	cbvraldva2 2736*	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 2737*	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.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	cbvraldva 2738*	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 2739*	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	cbvral2vw 2740*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2742 with a disjoint variable condition, which does not require ax-13 2169. (Contributed by NM, 10-Aug-2004.) (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2vw 2741*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2743 with a disjoint variable condition, which does not require ax-13 2169. (Contributed by FL, 2-Jul-2012.) (Revised by GG, 10-Jan-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	cbvral2v 2742*	Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓)
Theorem	cbvrex2v 2743*	Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓)
Theorem	cbvral3v 2744*	Change bound variables of triple restricted universal quantification, using implicit substitution. (Contributed by NM, 10-May-2005.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓)
Theorem	cbvralsv 2745*	Change bound variable by using a substitution. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	cbvrexsv 2746*	Change bound variable by using a substitution. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑)
Theorem	sbralie 2747*	Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓)
Theorem	rabbiia 2748	Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbii 2749	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2752. (Contributed by Peter Mazsa, 1-Nov-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabbidva2 2750*	Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabbidva 2751*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabbidv 2752*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	rabeqf 2753	Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	rabeqif 2754	Equality theorem for restricted class abstractions. Inference form of rabeqf 2753. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	rabeq 2755*	Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
Theorem	rabeqi 2756*	Equality theorem for restricted class abstractions. Inference form of rabeq 2755. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	rabeqdv 2757*	Equality of restricted class abstractions. Deduction form of rabeq 2755. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	rabeqbidv 2758*	Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabeqbidva 2759*	Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	rabeq2i 2760	Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
Theorem	cbvrab 2761	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
Theorem	cbvrabv 2762*	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}
2.1.6  The universal class
Syntax	cvv 2763	Extend class notation to include the universal class symbol.
class V
Theorem	vjust 2764	Soundness justification theorem for df-v 2765. (Contributed by Rodolfo Medina, 27-Apr-2010.)
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦}
Definition	df-v 2765	Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. (Contributed by NM, 5-Aug-1993.)
⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
Theorem	vex 2766	All setvar variables are sets (see isset 2769). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
⊢ 𝑥 ∈ V
Theorem	elv 2767	Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2766), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ (𝑥 ∈ V → 𝜑)    ⇒   ⊢ 𝜑
Theorem	elvd 2768	Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2766) and another antecedent, then it is implied by the other antecedent. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	isset 2769*	Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2765) if and only if the class 𝐴 exists (i.e. there exists some set 𝑥 equal to class 𝐴). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "𝐴 ∈ V " to mean "𝐴 is a set" very frequently, for example in uniex 4472. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4474, in order to shorten certain proofs we use the more general antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set." Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 2192 requires that the expression substituted for 𝐵 not contain 𝑥. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	issetf 2770	A version of isset that does not require x and A to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
Theorem	isseti 2771*	A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	issetri 2772*	A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥 𝑥 = 𝐴    ⇒   ⊢ 𝐴 ∈ V
Theorem	eqvisset 2773	A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 2769 and issetri 2772. (Contributed by BJ, 27-Apr-2019.)
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)
Theorem	elex 2774	If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
Theorem	elexi 2775	If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	elexd 2776	If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	elisset 2777*	An element of a class exists. (Contributed by NM, 1-May-1995.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	elex22 2778*	If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
Theorem	elex2 2779*	If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)
Theorem	ralv 2780	A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑)
Theorem	rexv 2781	An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Theorem	reuv 2782	A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.)
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑)
Theorem	rmov 2783	An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑)
Theorem	rabab 2784	A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ {𝑥 ∈ V ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	ralcom4 2785*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4 2786*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4a 2787*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓))
Theorem	rexcom4b 2788*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	ceqsalt 2789*	Closed theorem version of ceqsalg 2791. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsralt 2790*	Restricted quantifier version of ceqsalt 2789. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsalg 2791*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsal 2792*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsalv 2793*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsralv 2794*	Restricted quantifier version of ceqsalv 2793. (Contributed by NM, 21-Jun-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	gencl 2795*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵))    &   ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (𝜃 → 𝜓)
Theorem	2gencl 2796*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶)    &   ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷)    &   ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒)
Theorem	3gencl 2797*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐷)    &   ⊢ (𝐹 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐹)    &   ⊢ (𝐺 ∈ 𝑆 ↔ ∃𝑧 ∈ 𝑅 𝐶 = 𝐺)    &   ⊢ (𝐴 = 𝐷 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐹 → (𝜓 ↔ 𝜒))    &   ⊢ (𝐶 = 𝐺 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆) → 𝜃)
Theorem	cgsexg 2798*	Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007.)
⊢ (𝑥 = 𝐴 → 𝜒)    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝜒 ∧ 𝜑) ↔ 𝜓))
Theorem	cgsex2g 2799*	Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝜒)    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(𝜒 ∧ 𝜑) ↔ 𝜓))
Theorem	cgsex4g 2800*	An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.)
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒)    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓))