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	r19.43 2701	Restricted version of Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) (Proof rewritten by Jim Kingdon, 5-Jun-2018.)
|- ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )
Theorem	r19.44av 2702*	One direction of a restricted quantifier version of Theorem 19.44 of [Margaris] p. 90. The other direction doesn't hold when A is empty. (Contributed by NM, 2-Apr-2004.)
|- ( E. x e. A ( ph \/ ps ) -> ( E. x e. A ph \/ ps ) )
Theorem	r19.45av 2703*	Restricted version of one direction of Theorem 19.45 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.) (Contributed by NM, 2-Apr-2004.)
|- ( E. x e. A ( ph \/ ps ) -> ( ph \/ E. x e. A ps ) )
Theorem	ralcomf 2704*	Commutation of restricted quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ y A   &    |- F/_ x B   =>    |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
Theorem	rexcomf 2705*	Commutation of restricted quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ y A   &    |- F/_ x B   =>    |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )
Theorem	ralcom 2706*	Commutation of restricted quantifiers. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
Theorem	rexcom 2707*	Commutation of restricted quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )
Theorem	ralrot3 2708*	Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.)
|- ( A. x e. A A. y e. B A. z e. C ph <-> A. z e. C A. x e. A A. y e. B ph )
Theorem	rexcom13 2709*	Swap 1st and 3rd restricted existential quantifiers. (Contributed by NM, 8-Apr-2015.)
|- ( E. x e. A E. y e. B E. z e. C ph <-> E. z e. C E. y e. B E. x e. A ph )
Theorem	rexrot4 2710*	Rotate existential restricted quantifiers twice. (Contributed by NM, 8-Apr-2015.)
|- ( E. x e. A E. y e. B E. z e. C E. w e. D ph <-> E. z e. C E. w e. D E. x e. A E. y e. B ph )
Theorem	ralcom3 2711	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 2712*	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 2713*	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 2714*	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 2715	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 2716	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 2717*	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 2718*	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 2719	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	reqabi 2720	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	rabid2 2721*	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 2722	Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 2801. (Contributed by NM, 25-Nov-2013.)
|- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
Theorem	rabswap 2723	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 2724	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 2725*	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 2726	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 2727*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 2777 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 2728*	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 2729*	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 2730	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 2731	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 2732	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 2733*	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 2734*	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 2735	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 2736	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 2737	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 2738	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 2739	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 2740	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 2741*	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 2742*	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 2743*	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 2744*	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 2745*	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 2746*	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 2747*	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 2748*	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 2749*	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 2750*	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 2751*	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 2752*	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 2753*	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 2754*	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 2755*	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 2756*	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 2757*	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 2758*	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 2759*	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 2760*	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 2761	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 2762	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 2763	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
|- ( E! x e. A ph -> E. x e. A ph )
Theorem	reurmo 2764	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 2765	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 2766	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
|- ( -. E. x e. A ph -> E* x e. A ph )
Theorem	cbvralfw 2767*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 2769 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 1556 and ax-bndl 1558 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 2768*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2770 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 1556 and ax-bndl 1558 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 2769	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 2770	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 2771*	Rule used to change bound variables, using implicit substitution. Version of cbvral 2774 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 1556 and ax-bndl 1558 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 2772*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2768 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 1556 and ax-bndl 1558 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 2773*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 2776 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 2774*	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 2775*	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 2776*	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 2777*	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 2778*	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 2779*	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 2780*	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 2781*	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 2782*	Version of cbvralv 2778 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 2783*	Version of cbvrexv 2779 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 2784*	Version of cbvreuv 2780 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 2785*	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 2786*	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 2787*	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 2788*	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 2789*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2791 with a disjoint variable condition, which does not require ax-13 2205. (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 2790*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2792 with a disjoint variable condition, which does not require ax-13 2205. (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 2791*	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 2792*	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 2793*	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 2794*	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 2795*	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 2796*	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 2797*	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 2798	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 2799	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 2800	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2802. (Contributed by Peter Mazsa, 1-Nov-2019.)
|- ( ph <-> ps )   =>    |- { x e. A | ph } = { x e. A | ps }