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	reeanv 2701*	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 2702*	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 2703	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 2704	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 2705*	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 2706*	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 2707	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 2708*	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 2709	Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 2787. (Contributed by NM, 25-Nov-2013.)
|- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
Theorem	rabswap 2710	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 2711	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 2712*	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 2713	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 2714*	Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 2764 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 2715*	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 2716*	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 2717	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 2718	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 2719	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 2720*	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 2721*	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 2722	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 2723	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 2724	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 2725	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 2726	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 2727	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 2728*	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 2729*	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 2730*	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 2731*	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 2732*	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 2733*	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 2734*	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 2735*	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 2736*	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 2737*	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 2738*	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 2739*	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 2740*	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 2741*	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 2742*	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 2743*	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 2744*	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 2745*	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 2746*	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 2747*	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 2748	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 2749	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 2750	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
|- ( E! x e. A ph -> E. x e. A ph )
Theorem	reurmo 2751	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 2752	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 2753	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
|- ( -. E. x e. A ph -> E* x e. A ph )
Theorem	cbvralfw 2754*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 2756 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 1553 and ax-bndl 1555 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 2755*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2757 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 1553 and ax-bndl 1555 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 2756	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 2757	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 2758*	Rule used to change bound variables, using implicit substitution. Version of cbvral 2761 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 1553 and ax-bndl 1555 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 2759*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2755 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 1553 and ax-bndl 1555 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 2760*	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 2763 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 2761*	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 2762*	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 2763*	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 2764*	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 2765*	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 2766*	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 2767*	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 2768*	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 2769*	Version of cbvralv 2765 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 2770*	Version of cbvrexv 2766 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 2771*	Version of cbvreuv 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 ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
Theorem	cbvraldva2 2772*	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 2773*	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 2774*	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 2775*	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 2776*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2778 with a disjoint variable condition, which does not require ax-13 2202. (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 2777*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2779 with a disjoint variable condition, which does not require ax-13 2202. (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 2778*	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 2779*	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 2780*	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 2781*	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 2782*	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 2783*	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	rabbiia 2784	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 2785	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2788. (Contributed by Peter Mazsa, 1-Nov-2019.)
|- ( ph <-> ps )   =>    |- { x e. A | ph } = { x e. A | 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	rabbidva 2787*	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 2788*	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 2789	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 2790	Equality theorem for restricted class abstractions. Inference form of rabeqf 2789. (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 2791*	Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
|- ( A = B -> { x e. A | ph } = { x e. B | ph } )
Theorem	rabeqi 2792*	Equality theorem for restricted class abstractions. Inference form of rabeq 2791. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A = B   =>    |- { x e. A | ph } = { x e. B | ph }
Theorem	rabeqdv 2793*	Equality of restricted class abstractions. Deduction form of rabeq 2791. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ps } )
Theorem	rabeqbidv 2794*	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 2795*	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 2796	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 2797	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 }
Theorem	cbvrabv 2798*	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- { x e. A | ph } = { y e. A | ps }
2.1.6  The universal class
Syntax	cvv 2799	Extend class notation to include the universal class symbol.
class _V
Theorem	vjust 2800	Soundness justification theorem for df-v 2801. (Contributed by Rodolfo Medina, 27-Apr-2010.)
|- { x | x = x } = { y | y = y }