P. 27 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 2601-2700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	necon3bbid 2601	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- ( ph -> ( ps <-> A = B ) )   =>    |- ( ph -> ( -. ps <-> A =/= B ) )
Theorem	necon3bid 2602	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A = B <-> C = D ) )   =>    |- ( ph -> ( A =/= B <-> C =/= D ) )
Theorem	necon3ad 2603	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> -. ps ) )
Theorem	necon3bd 2604	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A = B -> ps ) )   =>    |- ( ph -> ( -. ps -> A =/= B ) )
Theorem	necon3d 2605	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	necon3i 2606	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
|- ( A = B -> C = D )   =>    |- ( C =/= D -> A =/= B )
Theorem	necon3ai 2607	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A = B )   =>    |- ( A =/= B -> -. ph )
Theorem	necon3bi 2608	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A = B -> ph )   =>    |- ( -. ph -> A =/= B )
Theorem	necon1ai 2609	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.)
|- ( -. ph -> A = B )   =>    |- ( A =/= B -> ph )
Theorem	necon1bi 2610	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A =/= B -> ph )   =>    |- ( -. ph -> A = B )
Theorem	necon1i 2611	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A =/= B -> C = D )   =>    |- ( C =/= D -> A = B )
Theorem	necon2ai 2612	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A = B -> -. ph )   =>    |- ( ph -> A =/= B )
Theorem	necon2bi 2613	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- ( ph -> A =/= B )   =>    |- ( A = B -> -. ph )
Theorem	necon2i 2614	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A = B -> C =/= D )   =>    |- ( C = D -> A =/= B )
Theorem	necon2ad 2615	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A = B -> -. ps ) )   =>    |- ( ph -> ( ps -> A =/= B ) )
Theorem	necon2bd 2616	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon2d 2617	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon1abii 2618	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.)
|- ( -. ph <-> A = B )   =>    |- ( A =/= B <-> ph )
Theorem	necon1bbii 2619	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.)
|- ( A =/= B <-> ph )   =>    |- ( -. ph <-> A = B )
Theorem	necon1abid 2620	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.)
|- ( ph -> ( -. ps <-> A = B ) )   =>    |- ( ph -> ( A =/= B <-> ps ) )
Theorem	necon1bbid 2621	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
|- ( ph -> ( A =/= B <-> ps ) )   =>    |- ( ph -> ( -. ps <-> A = B ) )
Theorem	necon2abii 2622	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
|- ( A = B <-> -. ph )   =>    |- ( ph <-> A =/= B )
Theorem	necon2bbii 2623	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A =/= B )   =>    |- ( A = B <-> -. ph )
Theorem	necon2abid 2624	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.)
|- ( ph -> ( A = B <-> -. ps ) )   =>    |- ( ph -> ( ps <-> A =/= B ) )
Theorem	necon2bbid 2625	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps <-> A =/= B ) )   =>    |- ( ph -> ( A = B <-> -. ps ) )
Theorem	necon4ai 2626	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A =/= B -> -. ph )   =>    |- ( ph -> A = B )
Theorem	necon4i 2627	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A =/= B -> C =/= D )   =>    |- ( C = D -> A = B )
Theorem	necon4ad 2628	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A =/= B -> -. ps ) )   =>    |- ( ph -> ( ps -> A = B ) )
Theorem	necon4bd 2629	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( -. ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> ps ) )
Theorem	necon4d 2630	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A =/= B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A = B ) )
Theorem	necon4abid 2631	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.)
|- ( ph -> ( A =/= B <-> -. ps ) )   =>    |- ( ph -> ( A = B <-> ps ) )
Theorem	necon4bbid 2632	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
|- ( ph -> ( -. ps <-> A =/= B ) )   =>    |- ( ph -> ( ps <-> A = B ) )
Theorem	necon4bid 2633	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
|- ( ph -> ( A =/= B <-> C =/= D ) )   =>    |- ( ph -> ( A = B <-> C = D ) )
Theorem	necon1ad 2634	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.)
|- ( ph -> ( -. ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> ps ) )
Theorem	necon1bd 2635	Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A =/= B -> ps ) )   =>    |- ( ph -> ( -. ps -> A = B ) )
Theorem	necon1d 2636	Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A =/= B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A = B ) )
Theorem	neneqad 2637	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2583. One-way deduction form of df-ne 2569. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	nebi 2638	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ( A = B <-> C = D ) <-> ( A =/= B <-> C =/= D ) )
Theorem	pm13.18 2639	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ A =/= C ) -> B =/= C )
Theorem	pm13.181 2640	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ B =/= C ) -> A =/= C )
Theorem	pm2.21ddne 2641	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ps )
Theorem	pm2.61ne 2642	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A = B -> ( ps <-> ch ) )   &    |- ( ( ph /\ A =/= B ) -> ps )   &    |- ( ph -> ch )   =>    |- ( ph -> ps )
Theorem	pm2.61ine 2643	Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A = B -> ph )   &    |- ( A =/= B -> ph )   =>    |- ph
Theorem	pm2.61dne 2644	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> ( A = B -> ps ) )   &    |- ( ph -> ( A =/= B -> ps ) )   =>    |- ( ph -> ps )
Theorem	pm2.61dane 2645	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
|- ( ( ph /\ A = B ) -> ps )   &    |- ( ( ph /\ A =/= B ) -> ps )   =>    |- ( ph -> ps )
Theorem	pm2.61da2ne 2646	Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
|- ( ( ph /\ A = B ) -> ps )   &    |- ( ( ph /\ C = D ) -> ps )   &    |- ( ( ph /\ ( A =/= B /\ C =/= D ) ) -> ps )   =>    |- ( ph -> ps )
Theorem	pm2.61da3ne 2647	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.)
|- ( ( ph /\ A = B ) -> ps )   &    |- ( ( ph /\ C = D ) -> ps )   &    |- ( ( ph /\ E = F ) -> ps )   &    |- ( ( ph /\ ( A =/= B /\ C =/= D /\ E =/= F ) ) -> ps )   =>    |- ( ph -> ps )
Theorem	necom 2648	Commutation of inequality. (Contributed by NM, 14-May-1999.)
|- ( A =/= B <-> B =/= A )
Theorem	necomi 2649	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
|- A =/= B   =>    |- B =/= A
Theorem	necomd 2650	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
|- ( ph -> A =/= B )   =>    |- ( ph -> B =/= A )
Theorem	neor 2651	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
|- ( ( A = B \/ ps ) <-> ( A =/= B -> ps ) )
Theorem	neanior 2652	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ( ( A =/= B /\ C =/= D ) <-> -. ( A = B \/ C = D ) )
Theorem	ne3anior 2653	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
|- ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( A = B \/ C = D \/ E = F ) )
Theorem	neorian 2654	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ( ( A =/= B \/ C =/= D ) <-> -. ( A = B /\ C = D ) )
Theorem	nemtbir 2655	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
|- A =/= B   &    |- ( ph <-> A = B )   =>    |- -. ph
Theorem	nelne1 2656	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
|- ( ( A e. B /\ -. A e. C ) -> B =/= C )
Theorem	nelne2 2657	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
|- ( ( A e. C /\ -. B e. C ) -> A =/= B )
Theorem	nfne 2658	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A =/= B
Theorem	nfned 2659	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A =/= B )
2.1.4.2  Negated membership
Theorem	neleq1 2660	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- ( A = B -> ( A e/ C <-> B e/ C ) )
Theorem	neleq2 2661	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- ( A = B -> ( C e/ A <-> C e/ B ) )
Theorem	neleq12d 2662	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A e/ C <-> B e/ D ) )
Theorem	nfnel 2663	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e/ B
Theorem	nfneld 2664	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e/ B )
Theorem	nnel 2665	Negation of negated membership, analogous to nne 2571. (Contributed by Alexander van der Vekens, 18-Jan-2018.)
|- ( -. A e/ B <-> A e. B )
2.1.5  Restricted quantification
Syntax	wral 2666	Extend wff notation to include restricted universal quantification.
wff A. x e. A ph
Syntax	wrex 2667	Extend wff notation to include restricted existential quantification.
wff E. x e. A ph
Syntax	wreu 2668	Extend wff notation to include restricted existential uniqueness.
wff E! x e. A ph
Syntax	wrmo 2669	Extend wff notation to include restricted "at most one."
wff E* x e. A ph
Syntax	crab 2670	Extend class notation to include the restricted class abstraction (class builder).
class { x e. A | ph }
Definition	df-ral 2671	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
Definition	df-rex 2672	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
Definition	df-reu 2673	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
Definition	df-rmo 2674	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
Definition	df-rab 2675	Define a restricted class abstraction (class builder), which is the class of all x in A such that ph is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
Theorem	ralnex 2676	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
|- ( A. x e. A -. ph <-> -. E. x e. A ph )
Theorem	rexnal 2677	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
|- ( E. x e. A -. ph <-> -. A. x e. A ph )
Theorem	dfral2 2678	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
|- ( A. x e. A ph <-> -. E. x e. A -. ph )
Theorem	dfrex2 2679	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
|- ( E. x e. A ph <-> -. A. x e. A -. ph )
Theorem	ralbida 2680	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbida 2681	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	ralbidva 2682*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidva 2683*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbid 2684	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbid 2685	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	ralbidv 2686*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidv 2687*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidv2 2688*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
|- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexbidv2 2689*	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	ralbii 2690	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( A. x e. A ph <-> A. x e. A ps )
Theorem	rexbii 2691	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( E. x e. A ph <-> E. x e. A ps )
Theorem	2ralbii 2692	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
|- ( ph <-> ps )   =>    |- ( A. x e. A A. y e. B ph <-> A. x e. A A. y e. B ps )
Theorem	2rexbii 2693	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	ralbii2 2694	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
|- ( ( x e. A -> ph ) <-> ( x e. B -> ps ) )   =>    |- ( A. x e. A ph <-> A. x e. B ps )
Theorem	rexbii2 2695	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	raleqbii 2696	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
|- A = B   &    |- ( ps <-> ch )   =>    |- ( A. x e. A ps <-> A. x e. B ch )
Theorem	rexeqbii 2697	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	ralbiia 2698	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. x e. A ps )
Theorem	rexbiia 2699	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	2rexbiia 2700*	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 )