P. 31 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3001-3100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nrexdv 3001*	Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.)
|- ( ( ph /\ x e. A ) -> -. ps )   =>    |- ( ph -> -. E. x e. A ps )
Theorem	rexex 3002	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
|- ( E. x e. A ph -> E. x ph )
Theorem	rspe 3003	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|- ( ( x e. A /\ ph ) -> E. x e. A ph )
Theorem	rsp2e 3004	Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof shortened by Wolf Lammen, 7-Jan-2020.)
|- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph )
Theorem	nfre1 3005	The setvar x is not free in E. x e. A ph. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x E. x e. A ph
Theorem	nfrexd 3006	Deduction version of nfrex 3007. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E. y e. A ps )
Theorem	nfrex 3007	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x E. y e. A ph
Theorem	rexim 3008	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )
Theorem	reximia 3009	Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
|- ( x e. A -> ( ph -> ps ) )   =>    |- ( E. x e. A ph -> E. x e. A ps )
Theorem	reximi2 3010	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
|- ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) )   =>    |- ( E. x e. A ph -> E. x e. B ps )
Theorem	reximi 3011	Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> E. x e. A ps )
Theorem	reximdai 3012	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
|- F/ x ph   &    |- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximd2a 3013	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020.)
|- F/ x ph   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> x e. B )   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> E. x e. B ch )
Theorem	reximdv2 3014*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )
Theorem	reximdvai 3015*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.)
|- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximdv 3016*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximdva 3017*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximddv 3018*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> E. x e. A ch )
Theorem	reximdvva 3019*	Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by AV, 5-Jan-2022.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps -> E. x e. A E. y e. B ch ) )
Theorem	reximddv2 3020*	Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A E. y e. B ps )   =>    |- ( ph -> E. x e. A E. y e. B ch )
Theorem	r19.23t 3021	Closed theorem form of r19.23 3022. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
|- ( F/ x ps -> ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) ) )
Theorem	r19.23 3022	Restricted quantifier version of 19.23 2080. See r19.23v 3023 for a version requiring fewer axioms. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.)
|- F/ x ps   =>    |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )
Theorem	r19.23v 3023*	Restricted quantifier version of 19.23v 1902. Version of r19.23 3022 with a dv condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
|- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )
Theorem	rexlimi 3024	Restricted quantifier version of exlimi 2086. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- F/ x ps   &    |- ( x e. A -> ( ph -> ps ) )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimd2 3025	Version of rexlimd 3026 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimd 3026	Deduction form of rexlimd 3026. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimiv 3027*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
|- ( x e. A -> ( ph -> ps ) )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimiva 3028*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
|- ( ( x e. A /\ ph ) -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimivw 3029*	Weaker version of rexlimiv 3027. (Contributed by FL, 19-Sep-2011.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimdv 3030*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
|- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdva 3031*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdvaa 3032*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdv3a 3033*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3030. (Contributed by NM, 7-Jun-2015.)
|- ( ( ph /\ x e. A /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdvw 3034*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimddv 3035*	Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
|- ( ph -> E. x e. A ps )   &    |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   =>    |- ( ph -> ch )
Theorem	rexlimivv 3036*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
|- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )   =>    |- ( E. x e. A E. y e. B ph -> ps )
Theorem	rexlimdvv 3037*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
|- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )
Theorem	rexlimdvva 3038*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )
Theorem	rexbii2 3039	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
|- ( ( x e. A /\ ph ) <-> ( x e. B /\ ps ) )   =>    |- ( E. x e. A ph <-> E. x e. B ps )
Theorem	rexbiia 3040	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. x e. A ps )
Theorem	rexbii 3041	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Dec-2019.)
|- ( ph <-> ps )   =>    |- ( E. x e. A ph <-> E. x e. A ps )
Theorem	2rexbii 3042	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
|- ( ph <-> ps )   =>    |- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )
Theorem	rexnal2 3043	Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( E. x e. A E. y e. B -. ph <-> -. A. x e. A A. y e. B ph )
Theorem	rexnal3 3044	Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.)
|- ( E. x e. A E. y e. B E. z e. C -. ph <-> -. A. x e. A A. y e. B A. z e. C ph )
Theorem	ralnex2 3045	Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A. x e. A A. y e. B -. ph <-> -. E. x e. A E. y e. B ph )
Theorem	ralnex3 3046	Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.)
|- ( A. x e. A A. y e. B A. z e. C -. ph <-> -. E. x e. A E. y e. B E. z e. C ph )
Theorem	rexbida 3047	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	rexbidv2 3048*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	rexbidva 3049*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	rexbidvaALT 3050*	Alternate proof of rexbida 3047, shorter but requires more axioms. (Contributed by NM, 9-Mar-1997.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	rexbid 3051	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	rexbidv 3052*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	rexbidvALT 3053*	Alternate proof of rexbidv 3052, shorter but requires more axioms. (Contributed by NM, 20-Nov-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	rexeqbii 3054	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
|- A = B   &    |- ( ps <-> ch )   =>    |- ( E. x e. A ps <-> E. x e. B ch )
Theorem	2rexbiia 3055*	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
|- ( ( x e. A /\ y e. B ) -> ( ph <-> ps ) )   =>    |- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )
Theorem	2rexbidva 3056*	Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )
Theorem	2rexbidv 3057*	Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )
Theorem	rexralbidv 3058*	Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A A. y e. B ps <-> E. x e. A A. y e. B ch ) )
Theorem	r2exlem 3059	Lemma factoring out common proof steps in r2exf 3060 an r2ex 3061. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.)
|- ( A. x e. A A. y e. B -. ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> -. ph ) )   =>    |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
Theorem	r2exf 3060*	Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2exlem 3059. (Revised by Wolf Lammen, 10-Jan-2020.)
|- F/_ y A   =>    |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
Theorem	r2ex 3061*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.)
|- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
Theorem	risset 3062*	Two ways to say " A belongs to B." (Contributed by NM, 22-Nov-1994.)
|- ( A e. B <-> E. x e. B x = A )
Theorem	r19.12 3063*	Restricted quantifier version of 19.12 2164. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( E. x e. A A. y e. B ph -> A. y e. B E. x e. A ph )
Theorem	r19.26 3064	Restricted quantifier version of 19.26 1798. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )
Theorem	r19.26-2 3065	Restricted quantifier version of 19.26-2 1799. Version of r19.26 3064 with two quantifiers. (Contributed by NM, 10-Aug-2004.)
|- ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A A. y e. B ph /\ A. x e. A A. y e. B ps ) )
Theorem	r19.26-3 3066	Version of r19.26 3064 with three quantifiers. (Contributed by FL, 22-Nov-2010.)
|- ( A. x e. A ( ph /\ ps /\ ch ) <-> ( A. x e. A ph /\ A. x e. A ps /\ A. x e. A ch ) )
Theorem	r19.26m 3067	Version of 19.26 1798 and r19.26 3064 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.)
|- ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ps ) ) <-> ( A. x e. A ph /\ A. x e. B ps ) )
Theorem	ralbi 3068	Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1746. (Contributed by NM, 6-Oct-2003.)
|- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ph <-> A. x e. A ps ) )
Theorem	ralbiim 3069	Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1816. (Contributed by NM, 3-Jun-2012.)
|- ( A. x e. A ( ph <-> ps ) <-> ( A. x e. A ( ph -> ps ) /\ A. x e. A ( ps -> ph ) ) )
Theorem	r19.27v 3070*	Restricted quantitifer version of one direction of 19.27 2095. (The other direction holds when A is nonempty, see r19.27zv 4071.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( ( A. x e. A ph /\ ps ) -> A. x e. A ( ph /\ ps ) )
Theorem	r19.28v 3071*	Restricted quantifier version of one direction of 19.28 2096. (The other direction holds when A is nonempty, see r19.28zv 4066.) (Contributed by NM, 2-Apr-2004.)
|- ( ( ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
Theorem	r19.29 3072	Restricted quantifier version of 19.29 1801. See also r19.29r 3073. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( ( A. x e. A ph /\ E. x e. A ps ) -> E. x e. A ( ph /\ ps ) )
Theorem	r19.29r 3073	Restricted quantifier version of 19.29r 1802; variation of r19.29 3072. (Contributed by NM, 31-Aug-1999.)
|- ( ( E. x e. A ph /\ A. x e. A ps ) -> E. x e. A ( ph /\ ps ) )
Theorem	r19.29imd 3074	Theorem 19.29 of [Margaris] p. 90 with an implication in the hypothesis containing the generalization, deduction version. (Contributed by AV, 19-Jan-2019.)
|- ( ph -> E. x e. A ps )   &    |- ( ph -> A. x e. A ( ps -> ch ) )   =>    |- ( ph -> E. x e. A ( ps /\ ch ) )
Theorem	r19.29af2 3075	A commonly used pattern based on r19.29 3072. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	r19.29af 3076*	A commonly used pattern based on r19.29 3072. (Contributed by Thierry Arnoux, 29-Nov-2017.)
|- F/ x ph   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	r19.29an 3077*	A commonly used pattern based on r19.29 3072. (Contributed by Thierry Arnoux, 29-Dec-2019.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   =>    |- ( ( ph /\ E. x e. A ps ) -> ch )
Theorem	r19.29a 3078*	A commonly used pattern based on r19.29 3072. (Contributed by Thierry Arnoux, 22-Nov-2017.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	2r19.29 3079	Theorem r19.29 3072 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.)
|- ( ( A. x e. A A. y e. B ph /\ E. x e. A E. y e. B ps ) -> E. x e. A E. y e. B ( ph /\ ps ) )
Theorem	r19.29d2r 3080	Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> A. x e. A A. y e. B ps )   &    |- ( ph -> E. x e. A E. y e. B ch )   =>    |- ( ph -> E. x e. A E. y e. B ( ps /\ ch ) )
Theorem	r19.29vva 3081*	A commonly used pattern based on r19.29 3072, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A E. y e. B ps )   =>    |- ( ph -> ch )
Theorem	r19.30 3082	Restricted quantifier version of 19.30 1809. (Contributed by Scott Fenton, 25-Feb-2011.)
|- ( A. x e. A ( ph \/ ps ) -> ( A. x e. A ph \/ E. x e. A ps ) )
Theorem	r19.32v 3083*	Restricted quantifier version of 19.32v 1869. (Contributed by NM, 25-Nov-2003.)
|- ( A. x e. A ( ph \/ ps ) <-> ( ph \/ A. x e. A ps ) )
Theorem	r19.35 3084	Restricted quantifier version of 19.35 1805. (Contributed by NM, 20-Sep-2003.)
|- ( E. x e. A ( ph -> ps ) <-> ( A. x e. A ph -> E. x e. A ps ) )
Theorem	r19.36v 3085*	Restricted quantifier version of one direction of 19.36 2098. (The other direction holds iff A is nonempty, see r19.36zv 4072.) (Contributed by NM, 22-Oct-2003.)
|- ( E. x e. A ( ph -> ps ) -> ( A. x e. A ph -> ps ) )
Theorem	r19.37 3086	Restricted quantifier version of one direction of 19.37 2100. (The other direction does not hold when A is empty.) (Contributed by FL, 13-May-2012.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/ x ph   =>    |- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) )
Theorem	r19.37v 3087*	Restricted quantifier version of one direction of 19.37v 1910. (The other direction holds iff A is nonempty, see r19.37zv 4067.) (Contributed by NM, 2-Apr-2004.)
|- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) )
Theorem	r19.40 3088	Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.)
|- ( E. x e. A ( ph /\ ps ) -> ( E. x e. A ph /\ E. x e. A ps ) )
Theorem	r19.41v 3089*	Restricted quantifier version 19.41v 1914. Version of r19.41 3090 with a dv condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)
|- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )
Theorem	r19.41 3090	Restricted quantifier version of 19.41 2103. See r19.41v 3089 for a version with a dv condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010.)
|- F/ x ps   =>    |- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )
Theorem	r19.41vv 3091*	Version of r19.41v 3089 with two quantifiers. (Contributed by Thierry Arnoux, 25-Jan-2017.)
|- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A E. y e. B ph /\ ps ) )
Theorem	r19.42v 3092*	Restricted quantifier version of 19.42v 1918 (see also 19.42 2105). (Contributed by NM, 27-May-1998.)
|- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )
Theorem	r19.43 3093	Restricted quantifier version of 19.43 1810. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )
Theorem	r19.44v 3094*	One direction of a restricted quantifier version of 19.44 2106. The other direction holds when A is nonempty, see r19.44zv 4069. (Contributed by NM, 2-Apr-2004.)
|- ( E. x e. A ( ph \/ ps ) -> ( E. x e. A ph \/ ps ) )
Theorem	r19.45v 3095*	Restricted quantifier version of one direction of 19.45 2107. The other direction holds when A is nonempty, see r19.45zv 4068. (Contributed by NM, 2-Apr-2004.)
|- ( E. x e. A ( ph \/ ps ) -> ( ph \/ E. x e. A ps ) )
Theorem	ralcomf 3096*	Commutation of restricted universal 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 3097*	Commutation of restricted existential 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 3098*	Commutation of restricted universal quantifiers. See ralcom2 3104 for a version without DV condition on x , y. (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 3099*	Commutation of restricted existential 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	ralcom13 3100*	Swap first and third 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. y e. B A. x e. A ph )