P. 27 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2601-2700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	neor 2601	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
|- ((A = B \/ ps) <-> (A =/= B -> ps))
Theorem	neanior 2602	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ((A =/= B /\ C =/= D) <-> -. (A = B \/ C = D))
Theorem	ne3anior 2603	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 2604	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ((A =/= B \/ C =/= D) <-> -. (A = B /\ C = D))
Theorem	nemtbir 2605	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
|- A =/= B   &   |- (ph <-> A = B)   =>   |- -. ph
Theorem	nelne1 2606	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 2607	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	neleq1 2608	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- (A = B -> (A e/ C <-> B e/ C))
Theorem	neleq2 2609	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- (A = B -> (C e/ A <-> C e/ B))
Theorem	neleq12d 2610	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	nfne 2611	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A =/= B
Theorem	nfnel 2612	Bound-variable hypothesis builder for inequality. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   &   |- F/_xB   =>   |- F/x A e/ B
Theorem	nfned 2613	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/x A =/= B)
Theorem	nfneld 2614	Bound-variable hypothesis builder for inequality. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/x A e/ B)
2.1.5  Restricted quantification
Syntax	wral 2615	Extend wff notation to include restricted universal quantification.
wff A.x e. A ph
Syntax	wrex 2616	Extend wff notation to include restricted existential quantification.
wff E.x e. A ph
Syntax	wreu 2617	Extend wff notation to include restricted existential uniqueness.
wff E!x e. A ph
Syntax	wrmo 2618	Extend wff notation to include restricted "at most one."
wff E*x e. A ph
Syntax	crab 2619	Extend class notation to include the restricted class abstraction (class builder).
class {x e. A | ph}
Definition	df-ral 2620	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 2621	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 2622	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
|- (E!x e. A ph <-> E!x(x e. A /\ ph))
Definition	df-rmo 2623	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 2624	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 2625	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 2626	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 2627	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 2628	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 2629	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
|- F/xph   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbida 2630	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
|- F/xph   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidva 2631*	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 2632*	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 2633	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
|- F/xph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	rexbid 2634	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
|- F/xph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	ralbidv 2635*	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 2636*	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 2637*	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 2638*	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 2639	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 2640	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 2641	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 2642	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 2643	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 2644	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 2645	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 2646	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 2647	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 2648	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 2649*	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	r2alf 2650*	Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_yA   =>   |- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))
Theorem	r2exf 2651*	Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_yA   =>   |- (E.x e. A E.y e. B ph <-> E.xE.y((x e. A /\ y e. B) /\ ph))
Theorem	r2al 2652*	Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
|- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))
Theorem	r2ex 2653*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
|- (E.x e. A E.y e. B ph <-> E.xE.y((x e. A /\ y e. B) /\ ph))
Theorem	2ralbida 2654*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.)
|- F/xph   &   |- F/yph   &   |- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	2ralbidva 2655*	Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
|- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	2rexbidva 2656*	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	2ralbidv 2657*	Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	2rexbidv 2658*	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 2659*	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	ralinexa 2660	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
|- (A.x e. A (ph -> -. ps) <-> -. E.x e. A (ph /\ ps))
Theorem	rexanali 2661	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
|- (E.x e. A (ph /\ -. ps) <-> -. A.x e. A (ph -> ps))
Theorem	risset 2662*	Two ways to say "A belongs to B." (Contributed by NM, 22-Nov-1994.)
|- (A e. B <-> E.x e. B x = A)
Theorem	hbral 2663	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
|- (y e. A -> A.x y e. A)   &   |- (ph -> A.xph)   =>   |- (A.y e. A ph -> A.xA.y e. A ph)
Theorem	hbra1 2664	x is not free in A.x e. Aph. (Contributed by NM, 18-Oct-1996.)
|- (A.x e. A ph -> A.xA.x e. A ph)
Theorem	nfra1 2665	x is not free in A.x e. Aph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/xA.x e. A ph
Theorem	nfrald 2666	Deduction version of nfral 2668. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/yph   &   |- (ph -> F/_xA)   &   |- (ph -> F/xps)   =>   |- (ph -> F/xA.y e. A ps)
Theorem	nfrexd 2667	Deduction version of nfrex 2670. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/yph   &   |- (ph -> F/_xA)   &   |- (ph -> F/xps)   =>   |- (ph -> F/xE.y e. A ps)
Theorem	nfral 2668	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   &   |- F/xph   =>   |- F/xA.y e. A ph
Theorem	nfra2 2669*	Similar to Lemma 24 of [Monk2] p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD in set.mm. Contributed by Alan Sare 31-Dec-2011. (Contributed by NM, 31-Dec-2011.)
|- F/yA.x e. A A.y e. B ph
Theorem	nfrex 2670	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   &   |- F/xph   =>   |- F/xE.y e. A ph
Theorem	nfre1 2671	x is not free in E.x e. Aph. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/xE.x e. A ph
Theorem	r3al 2672*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
|- (A.x e. A A.y e. B A.z e. C ph <-> A.xA.yA.z((x e. A /\ y e. B /\ z e. C) -> ph))
Theorem	alral 2673	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
|- (A.xph -> A.x e. A ph)
Theorem	rexex 2674	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
|- (E.x e. A ph -> E.xph)
Theorem	rsp 2675	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|- (A.x e. A ph -> (x e. A -> ph))
Theorem	rspe 2676	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|- ((x e. A /\ ph) -> E.x e. A ph)
Theorem	rsp2 2677	Restricted specialization. (Contributed by NM, 11-Feb-1997.)
|- (A.x e. A A.y e. B ph -> ((x e. A /\ y e. B) -> ph))
Theorem	rsp2e 2678	Restricted specialization. (Contributed by FL, 4-Jun-2012.)
|- ((x e. A /\ y e. B /\ ph) -> E.x e. A E.y e. B ph)
Theorem	rspec 2679	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- A.x e. A ph   =>   |- (x e. A -> ph)
Theorem	rgen 2680	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- (x e. A -> ph)   =>   |- A.x e. A ph
Theorem	rgen2a 2681*	Generalization rule for restricted quantification. Note that x and y needn't be distinct (and illustrates the use of dvelim 2016). (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.
|- ((x e. A /\ y e. A) -> ph)   =>   |- A.x e. A A.y e. A ph
Theorem	rgenw 2682	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
|- ph   =>   |- A.x e. A ph
Theorem	rgen2w 2683	Generalization rule for restricted quantification. Note that x and y needn't be distinct. (Contributed by NM, 18-Jun-2014.)
|- ph   =>   |- A.x e. A A.y e. B ph
Theorem	mprg 2684	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
|- (A.x e. A ph -> ps)   &   |- (x e. A -> ph)   =>   |- ps
Theorem	mprgbir 2685	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
|- (ph <-> A.x e. A ps)   &   |- (x e. A -> ps)   =>   |- ph
Theorem	ralim 2686	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
|- (A.x e. A (ph -> ps) -> (A.x e. A ph -> A.x e. A ps))
Theorem	ralimi2 2687	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
|- ((x e. A -> ph) -> (x e. B -> ps))   =>   |- (A.x e. A ph -> A.x e. B ps)
Theorem	ralimia 2688	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
|- (x e. A -> (ph -> ps))   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	ralimiaa 2689	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
|- ((x e. A /\ ph) -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	ralimi 2690	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
|- (ph -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	ral2imi 2691	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
|- (ph -> (ps -> ch))   =>   |- (A.x e. A ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	ralimdaa 2692	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)
|- F/xph   &   |- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	ralimdva 2693*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	ralimdv 2694*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	ralimdv2 2695*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
|- (ph -> ((x e. A -> ps) -> (x e. B -> ch)))   =>   |- (ph -> (A.x e. A ps -> A.x e. B ch))
Theorem	ralrimi 2696	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
|- F/xph   &   |- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	ralrimiv 2697*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
|- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	ralrimiva 2698*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
|- ((ph /\ x e. A) -> ps)   =>   |- (ph -> A.x e. A ps)
Theorem	ralrimivw 2699*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
|- (ph -> ps)   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21t 2700	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)
|- ( F/xph -> (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps)))