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	ralcom3 2701	A commutative law for restricted quantifiers that swaps the domain of the restriction. (Contributed by NM, 22-Feb-2004.)
|- ( A. x e. A ( x e. B -> ph ) <-> A. x e. B ( x e. A -> ph ) )
Theorem	reean 2702*	Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )
Theorem	reeanv 2703*	Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
|- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )
Theorem	3reeanv 2704*	Rearrange three existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.)
|- ( E. x e. A E. y e. B E. z e. C ( ph /\ ps /\ ch ) <-> ( E. x e. A ph /\ E. y e. B ps /\ E. z e. C ch ) )
Theorem	nfreu1 2705	x is not free in E! x e. A ph. (Contributed by NM, 19-Mar-1997.)
|- F/ x E! x e. A ph
Theorem	nfrmo1 2706	x is not free in E* x e. A ph. (Contributed by NM, 16-Jun-2017.)
|- F/ x E* x e. A ph
Theorem	nfreudxy 2707*	Not-free deduction for restricted uniqueness. This is a version where x and y are distinct. (Contributed by Jim Kingdon, 6-Jun-2018.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E! y e. A ps )
Theorem	nfreuw 2708*	Not-free for restricted uniqueness. This is a version where x and y are distinct. (Contributed by Jim Kingdon, 6-Jun-2018.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x E! y e. A ph
Theorem	rabid 2709	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.)
|- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )
Theorem	rabid2 2710*	An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( A = { x e. A | ph } <-> A. x e. A ph )
Theorem	rabbi 2711	Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 2790. (Contributed by NM, 25-Nov-2013.)
|- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
Theorem	rabswap 2712	Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.)
|- { x e. A | x e. B } = { x e. B | x e. A }
Theorem	nfrab1 2713	The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
|- F/_ x { x e. A | ph }
Theorem	nfrabw 2714*	A variable not free in a wff remains so in a restricted class abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.)
|- F/ x ph   &    |- F/_ x A   =>    |- F/_ x { y e. A | ph }
Theorem	reubida 2715	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) )
Theorem	cbvrmow 2716*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 2766 with a disjoint variable condition. (Contributed by NM, 16-Jun-2017.) (Revised by GG, 23-May-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x e. A ph <-> E* y e. A ps )
Theorem	reubidva 2717*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) )
Theorem	reubidv 2718*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x e. A ps <-> E! x e. A ch ) )
Theorem	reubiia 2719	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! x e. A ps )
Theorem	reubii 2720	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.)
|- ( ph <-> ps )   =>    |- ( E! x e. A ph <-> E! x e. A ps )
Theorem	rmobida 2721	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) )
Theorem	rmobidva 2722*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) )
Theorem	rmobidv 2723*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x e. A ps <-> E* x e. A ch ) )
Theorem	rmobiia 2724	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( E* x e. A ph <-> E* x e. A ps )
Theorem	rmobii 2725	Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.)
|- ( ph <-> ps )   =>    |- ( E* x e. A ph <-> E* x e. A ps )
Theorem	raleqf 2726	Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )
Theorem	rexeqf 2727	Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) )
Theorem	reueq1f 2728	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.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> ( E! x e. A ph <-> E! x e. B ph ) )
Theorem	rmoeq1f 2729	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.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> ( E* x e. A ph <-> E* x e. B ph ) )
Theorem	raleq 2730*	Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
|- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )
Theorem	rexeq 2731*	Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
|- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) )
Theorem	reueq1 2732*	Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.)
|- ( A = B -> ( E! x e. A ph <-> E! x e. B ph ) )
Theorem	rmoeq1 2733*	Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- ( A = B -> ( E* x e. A ph <-> E* x e. B ph ) )
Theorem	raleqi 2734*	Equality inference for restricted universal qualifier. (Contributed by Paul Chapman, 22-Jun-2011.)
|- A = B   =>    |- ( A. x e. A ph <-> A. x e. B ph )
Theorem	rexeqi 2735*	Equality inference for restricted existential qualifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- A = B   =>    |- ( E. x e. A ph <-> E. x e. B ph )
Theorem	raleqdv 2736*	Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
Theorem	rexeqdv 2737*	Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
|- ( ph -> A = B )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
Theorem	raleqtrdv 2738*	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> A. x e. A ps )   &    |- ( ph -> A = B )   =>    |- ( ph -> A. x e. B ps )
Theorem	rexeqtrdv 2739*	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> E. x e. A ps )   &    |- ( ph -> A = B )   =>    |- ( ph -> E. x e. B ps )
Theorem	raleqtrrdv 2740*	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> A. x e. A ps )   &    |- ( ph -> B = A )   =>    |- ( ph -> A. x e. B ps )
Theorem	rexeqtrrdv 2741*	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> E. x e. A ps )   &    |- ( ph -> B = A )   =>    |- ( ph -> E. x e. B ps )
Theorem	raleqbi1dv 2742*	Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
|- ( A = B -> ( ph <-> ps ) )   =>    |- ( A = B -> ( A. x e. A ph <-> A. x e. B ps ) )
Theorem	rexeqbi1dv 2743*	Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.)
|- ( A = B -> ( ph <-> ps ) )   =>    |- ( A = B -> ( E. x e. A ph <-> E. x e. B ps ) )
Theorem	reueqd 2744*	Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.)
|- ( A = B -> ( ph <-> ps ) )   =>    |- ( A = B -> ( E! x e. A ph <-> E! x e. B ps ) )
Theorem	rmoeqd 2745*	Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- ( A = B -> ( ph <-> ps ) )   =>    |- ( A = B -> ( E* x e. A ph <-> E* x e. B ps ) )
Theorem	raleqbidv 2746*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
|- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexeqbidv 2747*	Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
|- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	raleqbidva 2748*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexeqbidva 2749*	Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	mormo 2750	Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|- ( E* x ph -> E* x e. A ph )
Theorem	reu5 2751	Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
|- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
Theorem	reurex 2752	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
|- ( E! x e. A ph -> E. x e. A ph )
Theorem	reurmo 2753	Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
|- ( E! x e. A ph -> E* x e. A ph )
Theorem	rmo5 2754	Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
|- ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) )
Theorem	nrexrmo 2755	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
|- ( -. E. x e. A ph -> E* x e. A ph )
Theorem	cbvralfw 2756*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 2758 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 1555 and ax-bndl 1557 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by GG, 23-May-2024.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
Theorem	cbvrexfw 2757*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2759 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 1555 and ax-bndl 1557 in the proof. (Contributed by FL, 27-Apr-2008.) (Revised by GG, 10-Jan-2024.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
Theorem	cbvralf 2758	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
Theorem	cbvrexf 2759	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.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
Theorem	cbvralw 2760*	Rule used to change bound variables, using implicit substitution. Version of cbvral 2763 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 1555 and ax-bndl 1557 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
Theorem	cbvrexw 2761*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2757 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 1555 and ax-bndl 1557 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
Theorem	cbvreuw 2762*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 2765 with a disjoint variable condition. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Dec-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
Theorem	cbvral 2763*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
Theorem	cbvrex 2764*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
Theorem	cbvreu 2765*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
Theorem	cbvrmo 2766*	Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x e. A ph <-> E* y e. A ps )
Theorem	cbvralv 2767*	Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
Theorem	cbvrexv 2768*	Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
Theorem	cbvreuv 2769*	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.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
Theorem	cbvrmov 2770*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x e. A ph <-> E* y e. A ps )
Theorem	cbvralvw 2771*	Version of cbvralv 2767 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
Theorem	cbvrexvw 2772*	Version of cbvrexv 2768 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
Theorem	cbvreuvw 2773*	Version of cbvreuv 2769 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
Theorem	cbvraldva2 2774*	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.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   &    |- ( ( ph /\ x = y ) -> A = B )   =>    |- ( ph -> ( A. x e. A ps <-> A. y e. B ch ) )
Theorem	cbvrexdva2 2775*	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.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   &    |- ( ( ph /\ x = y ) -> A = B )   =>    |- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) )
Theorem	cbvraldva 2776*	Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. y e. A ch ) )
Theorem	cbvrexdva 2777*	Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. y e. A ch ) )
Theorem	cbvral2vw 2778*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2780 with a disjoint variable condition, which does not require ax-13 2204. (Contributed by NM, 10-Aug-2004.) (Revised by GG, 10-Jan-2024.)
|- ( x = z -> ( ph <-> ch ) )   &    |- ( y = w -> ( ch <-> ps ) )   =>    |- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )
Theorem	cbvrex2vw 2779*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2781 with a disjoint variable condition, which does not require ax-13 2204. (Contributed by FL, 2-Jul-2012.) (Revised by GG, 10-Jan-2024.)
|- ( x = z -> ( ph <-> ch ) )   &    |- ( y = w -> ( ch <-> ps ) )   =>    |- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps )
Theorem	cbvral2v 2780*	Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.)
|- ( x = z -> ( ph <-> ch ) )   &    |- ( y = w -> ( ch <-> ps ) )   =>    |- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )
Theorem	cbvrex2v 2781*	Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.)
|- ( x = z -> ( ph <-> ch ) )   &    |- ( y = w -> ( ch <-> ps ) )   =>    |- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps )
Theorem	cbvral3v 2782*	Change bound variables of triple restricted universal quantification, using implicit substitution. (Contributed by NM, 10-May-2005.)
|- ( x = w -> ( ph <-> ch ) )   &    |- ( y = v -> ( ch <-> th ) )   &    |- ( z = u -> ( th <-> ps ) )   =>    |- ( A. x e. A A. y e. B A. z e. C ph <-> A. w e. A A. v e. B A. u e. C ps )
Theorem	cbvralsv 2783*	Change bound variable by using a substitution. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- ( A. x e. A ph <-> A. y e. A [ y / x ] ph )
Theorem	cbvrexsv 2784*	Change bound variable by using a substitution. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.)
|- ( E. x e. A ph <-> E. y e. A [ y / x ] ph )
Theorem	sbralie 2785*	Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. y ph <-> [ y / x ] A. y e. x ps )
Theorem	rabbidva2 2786*	Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	rabbia2 2787	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) )   =>    |- { x e. A | ps } = { x e. B | ch }
Theorem	rabbiia 2788	Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- { x e. A | ph } = { x e. A | ps }
Theorem	rabbii 2789	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2791. (Contributed by Peter Mazsa, 1-Nov-2019.)
|- ( ph <-> ps )   =>    |- { x e. A | ph } = { x e. A | ps }
Theorem	rabbidva 2790*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	rabbidv 2791*	Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	rabeqf 2792	Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> { x e. A | ph } = { x e. B | ph } )
Theorem	rabeqif 2793	Equality theorem for restricted class abstractions. Inference form of rabeqf 2792. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x A   &    |- F/_ x B   &    |- A = B   =>    |- { x e. A | ph } = { x e. B | ph }
Theorem	rabeq 2794*	Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
|- ( A = B -> { x e. A | ph } = { x e. B | ph } )
Theorem	rabeqi 2795*	Equality theorem for restricted class abstractions. Inference form of rabeq 2794. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A = B   =>    |- { x e. A | ph } = { x e. B | ph }
Theorem	rabeqdv 2796*	Equality of restricted class abstractions. Deduction form of rabeq 2794. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ps } )
Theorem	rabeqbidv 2797*	Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)
|- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	rabeqbidva 2798*	Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	rabeq2i 2799	Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)
|- A = { x e. B | ph }   =>    |- ( x e. A <-> ( x e. B /\ ph ) )
Theorem	cbvrab 2800	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.)
|- F/_ x A   &    |- F/_ y A   &    |- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x e. A | ph } = { y e. A | ps }