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	raleq 2701*	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 2702*	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 2703*	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 2704*	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 2705*	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 2706*	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 2707*	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 2708*	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 2709*	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 2710*	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 2711*	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 2712*	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 2713*	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 2714*	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 2715*	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 2716*	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 2717*	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 2718*	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 2719*	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 2720*	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 2721	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 2722	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 2723	Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
|- ( E! x e. A ph -> E. x e. A ph )
Theorem	reurmo 2724	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 2725	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 2726	Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
|- ( -. E. x e. A ph -> E* x e. A ph )
Theorem	cbvralfw 2727*	Rule used to change bound variables, using implicit substitution. Version of cbvralf 2729 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 1529 and ax-bndl 1531 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 2728*	Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2730 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 1529 and ax-bndl 1531 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 2729	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 2730	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 2731*	Rule used to change bound variables, using implicit substitution. Version of cbvral 2733 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 1529 and ax-bndl 1531 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 2732*	Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2728 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 1529 and ax-bndl 1531 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	cbvral 2733*	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 2734*	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 2735*	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 2736*	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 2737*	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 2738*	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 2739*	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 2740*	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 2741*	Version of cbvralv 2737 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 2742*	Version of cbvrexv 2738 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 2743*	Version of cbvreuv 2739 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 2744*	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 2745*	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 2746*	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 2747*	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 2748*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2750 with a disjoint variable condition, which does not require ax-13 2177. (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 2749*	Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2751 with a disjoint variable condition, which does not require ax-13 2177. (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 2750*	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 2751*	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 2752*	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 2753*	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 2754*	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 2755*	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 2756	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 2757	Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 2760. (Contributed by Peter Mazsa, 1-Nov-2019.)
|- ( ph <-> ps )   =>    |- { x e. A | ph } = { x e. A | ps }
Theorem	rabbidva2 2758*	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 2759*	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 2760*	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 2761	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 2762	Equality theorem for restricted class abstractions. Inference form of rabeqf 2761. (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 2763*	Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
|- ( A = B -> { x e. A | ph } = { x e. B | ph } )
Theorem	rabeqi 2764*	Equality theorem for restricted class abstractions. Inference form of rabeq 2763. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A = B   =>    |- { x e. A | ph } = { x e. B | ph }
Theorem	rabeqdv 2765*	Equality of restricted class abstractions. Deduction form of rabeq 2763. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ps } )
Theorem	rabeqbidv 2766*	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 2767*	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 2768	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 2769	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 2770*	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 2771	Extend class notation to include the universal class symbol.
class _V
Theorem	vjust 2772	Soundness justification theorem for df-v 2773. (Contributed by Rodolfo Medina, 27-Apr-2010.)
|- { x | x = x } = { y | y = y }
Definition	df-v 2773	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 = { x | x = x }
Theorem	vex 2774	All setvar variables are sets (see isset 2777). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 5-Aug-1993.)
|- x e. _V
Theorem	elv 2775	Technical lemma used to shorten proofs. If a proposition is implied by x e. _V (which is true, see vex 2774), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)
|- ( x e. _V -> ph )   =>    |- ph
Theorem	elvd 2776	Technical lemma used to shorten proofs. If a proposition is implied by x e. _V (which is true, see vex 2774) and another antecedent, then it is implied by the other antecedent. (Contributed by Peter Mazsa, 23-Oct-2018.)
|- ( ( ph /\ x e. _V ) -> ps )   =>    |- ( ph -> ps )
Theorem	isset 2777*	Two ways to say " A is a set": A class A is a member of the universal class _V (see df-v 2773) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device " A e. _V " to mean " A is a set" very frequently, for example in uniex 4482. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4484, in order to shorten certain proofs we use the more general antecedent A e. V instead of A e. _V to mean " A 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 2200 requires that the expression substituted for B not contain x. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)
|- ( A e. _V <-> E. x x = A )
Theorem	issetf 2778	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.)
|- F/_ x A   =>    |- ( A e. _V <-> E. x x = A )
Theorem	isseti 2779*	A way to say " A is a set" (inference form). (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- E. x x = A
Theorem	issetri 2780*	A way to say " A is a set" (inference form). (Contributed by NM, 5-Aug-1993.)
|- E. x x = A   =>    |- A e. _V
Theorem	eqvisset 2781	A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 2777 and issetri 2780. (Contributed by BJ, 27-Apr-2019.)
|- ( x = A -> A e. _V )
Theorem	elex 2782	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.)
|- ( A e. B -> A e. _V )
Theorem	elexi 2783	If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)
|- A e. B   =>    |- A e. _V
Theorem	elexd 2784	If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   =>    |- ( ph -> A e. _V )
Theorem	elisset 2785*	An element of a class exists. (Contributed by NM, 1-May-1995.)
|- ( A e. V -> E. x x = A )
Theorem	elex22 2786*	If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) )
Theorem	elex2 2787*	If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)
|- ( A e. B -> E. x x e. B )
Theorem	ralv 2788	A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
|- ( A. x e. _V ph <-> A. x ph )
Theorem	rexv 2789	An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
|- ( E. x e. _V ph <-> E. x ph )
Theorem	reuv 2790	A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.)
|- ( E! x e. _V ph <-> E! x ph )
Theorem	rmov 2791	An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- ( E* x e. _V ph <-> E* x ph )
Theorem	rabab 2792	A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- { x e. _V | ph } = { x | ph }
Theorem	ralcom4 2793*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- ( A. x e. A A. y ph <-> A. y A. x e. A ph )
Theorem	rexcom4 2794*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- ( E. x e. A E. y ph <-> E. y E. x e. A ph )
Theorem	rexcom4a 2795*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
|- ( E. x E. y e. A ( ph /\ ps ) <-> E. y e. A ( ph /\ E. x ps ) )
Theorem	rexcom4b 2796*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
|- B e. _V   =>    |- ( E. x E. y e. A ( ph /\ x = B ) <-> E. y e. A ph )
Theorem	ceqsalt 2797*	Closed theorem version of ceqsalg 2799. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	ceqsralt 2798*	Restricted quantifier version of ceqsalt 2797. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A. x e. B ( x = A -> ph ) <-> ps ) )
Theorem	ceqsalg 2799*	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.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	ceqsal 2800*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
|- F/ x ps   &    |- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x ( x = A -> ph ) <-> ps )