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	neanior 2601	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((A ≠ B ∧ C ≠ D) ↔ ¬ (A = B ∨ C = D))
Theorem	ne3anior 2602	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 2603	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((A ≠ B ∨ C ≠ D) ↔ ¬ (A = B ∧ C = D))
Theorem	nemtbir 2604	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ A ≠ B    &   ⊢ (φ ↔ A = B)    ⇒   ⊢ ¬ φ
Theorem	nelne1 2605	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
⊢ ((A ∈ B ∧ ¬ A ∈ C) → B ≠ C)
Theorem	nelne2 2606	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
⊢ ((A ∈ C ∧ ¬ B ∈ C) → A ≠ B)
Theorem	neleq1 2607	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (A = B → (A ∉ C ↔ B ∉ C))
Theorem	neleq2 2608	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (A = B → (C ∉ A ↔ C ∉ B))
Theorem	neleq12d 2609	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A ∉ C ↔ B ∉ D))
Theorem	nfne 2610	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ≠ B
Theorem	nfnel 2611	Bound-variable hypothesis builder for inequality. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ∉ B
Theorem	nfned 2612	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ≠ B)
Theorem	nfneld 2613	Bound-variable hypothesis builder for inequality. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ∉ B)
2.1.5  Restricted quantification
Syntax	wral 2614	Extend wff notation to include restricted universal quantification.
wff ∀x ∈ A φ
Syntax	wrex 2615	Extend wff notation to include restricted existential quantification.
wff ∃x ∈ A φ
Syntax	wreu 2616	Extend wff notation to include restricted existential uniqueness.
wff ∃!x ∈ A φ
Syntax	wrmo 2617	Extend wff notation to include restricted "at most one."
wff ∃*x ∈ A φ
Syntax	crab 2618	Extend class notation to include the restricted class abstraction (class builder).
class {x ∈ A ∣ φ}
Definition	df-ral 2619	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
Definition	df-rex 2620	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
Definition	df-reu 2621	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
Definition	df-rmo 2622	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*x ∈ A φ ↔ ∃*x(x ∈ A ∧ φ))
Definition	df-rab 2623	Define a restricted class abstraction (class builder), which is the class of all x in A such that φ is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}
Theorem	ralnex 2624	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∀x ∈ A ¬ φ ↔ ¬ ∃x ∈ A φ)
Theorem	rexnal 2625	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∃x ∈ A ¬ φ ↔ ¬ ∀x ∈ A φ)
Theorem	dfral2 2626	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∀x ∈ A φ ↔ ¬ ∃x ∈ A ¬ φ)
Theorem	dfrex2 2627	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∃x ∈ A φ ↔ ¬ ∀x ∈ A ¬ φ)
Theorem	ralbida 2628	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbida 2629	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbidva 2630*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbidva 2631*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbid 2632	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbid 2633	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbidv 2634*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbidv 2635*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbidv2 2636*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)
⊢ (φ → ((x ∈ A → ψ) ↔ (x ∈ B → χ)))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B χ))
Theorem	rexbidv2 2637*	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
⊢ (φ → ((x ∈ A ∧ ψ) ↔ (x ∈ B ∧ χ)))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ B χ))
Theorem	ralbii 2638	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)
Theorem	rexbii 2639	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)
Theorem	2ralbii 2640	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x ∈ A ∀y ∈ B ψ)
Theorem	2rexbii 2641	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x ∈ A ∃y ∈ B ψ)
Theorem	ralbii2 2642	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
⊢ ((x ∈ A → φ) ↔ (x ∈ B → ψ))    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ B ψ)
Theorem	rexbii2 2643	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
⊢ ((x ∈ A ∧ φ) ↔ (x ∈ B ∧ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ B ψ)
Theorem	raleqbii 2644	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ A = B    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (∀x ∈ A ψ ↔ ∀x ∈ B χ)
Theorem	rexeqbii 2645	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
⊢ A = B    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (∃x ∈ A ψ ↔ ∃x ∈ B χ)
Theorem	ralbiia 2646	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
⊢ (x ∈ A → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)
Theorem	rexbiia 2647	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
⊢ (x ∈ A → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)
Theorem	2rexbiia 2648*	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
⊢ ((x ∈ A ∧ y ∈ B) → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x ∈ A ∃y ∈ B ψ)
Theorem	r2alf 2649*	Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ℲyA    ⇒   ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))
Theorem	r2exf 2650*	Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ ℲyA    ⇒   ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ))
Theorem	r2al 2651*	Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))
Theorem	r2ex 2652*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x∃y((x ∈ A ∧ y ∈ B) ∧ φ))
Theorem	2ralbida 2653*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 24-Feb-2004.)
⊢ Ⅎxφ    &   ⊢ Ⅎyφ    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	2ralbidva 2654*	Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	2rexbidva 2655*	Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
⊢ ((φ ∧ (x ∈ A ∧ y ∈ B)) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ ↔ ∃x ∈ A ∃y ∈ B χ))
Theorem	2ralbidv 2656*	Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ∀y ∈ B ψ ↔ ∀x ∈ A ∀y ∈ B χ))
Theorem	2rexbidv 2657*	Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∃y ∈ B ψ ↔ ∃x ∈ A ∃y ∈ B χ))
Theorem	rexralbidv 2658*	Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ∀y ∈ B ψ ↔ ∃x ∈ A ∀y ∈ B χ))
Theorem	ralinexa 2659	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
⊢ (∀x ∈ A (φ → ¬ ψ) ↔ ¬ ∃x ∈ A (φ ∧ ψ))
Theorem	rexanali 2660	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
⊢ (∃x ∈ A (φ ∧ ¬ ψ) ↔ ¬ ∀x ∈ A (φ → ψ))
Theorem	risset 2661*	Two ways to say "A belongs to B." (Contributed by NM, 22-Nov-1994.)
⊢ (A ∈ B ↔ ∃x ∈ B x = A)
Theorem	hbral 2662	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (φ → ∀xφ)    ⇒   ⊢ (∀y ∈ A φ → ∀x∀y ∈ A φ)
Theorem	hbra1 2663	x is not free in ∀x ∈ Aφ. (Contributed by NM, 18-Oct-1996.)
⊢ (∀x ∈ A φ → ∀x∀x ∈ A φ)
Theorem	nfra1 2664	x is not free in ∀x ∈ Aφ. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎx∀x ∈ A φ
Theorem	nfrald 2665	Deduction version of nfral 2667. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∀y ∈ A ψ)
Theorem	nfrexd 2666	Deduction version of nfrex 2669. (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃y ∈ A ψ)
Theorem	nfral 2667	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∀y ∈ A φ
Theorem	nfra2 2668*	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.)
⊢ Ⅎy∀x ∈ A ∀y ∈ B φ
Theorem	nfrex 2669	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∃y ∈ A φ
Theorem	nfre1 2670	x is not free in ∃x ∈ Aφ. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎx∃x ∈ A φ
Theorem	r3al 2671*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
⊢ (∀x ∈ A ∀y ∈ B ∀z ∈ C φ ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ B ∧ z ∈ C) → φ))
Theorem	alral 2672	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
⊢ (∀xφ → ∀x ∈ A φ)
Theorem	rexex 2673	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
⊢ (∃x ∈ A φ → ∃xφ)
Theorem	rsp 2674	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
⊢ (∀x ∈ A φ → (x ∈ A → φ))
Theorem	rspe 2675	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
⊢ ((x ∈ A ∧ φ) → ∃x ∈ A φ)
Theorem	rsp2 2676	Restricted specialization. (Contributed by NM, 11-Feb-1997.)
⊢ (∀x ∈ A ∀y ∈ B φ → ((x ∈ A ∧ y ∈ B) → φ))
Theorem	rsp2e 2677	Restricted specialization. (Contributed by FL, 4-Jun-2012.)
⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → ∃x ∈ A ∃y ∈ B φ)
Theorem	rspec 2678	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ ∀x ∈ A φ    ⇒   ⊢ (x ∈ A → φ)
Theorem	rgen 2679	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ (x ∈ A → φ)    ⇒   ⊢ ∀x ∈ A φ
Theorem	rgen2a 2680*	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 ∈ A ∧ y ∈ A) → φ)    ⇒   ⊢ ∀x ∈ A ∀y ∈ A φ
Theorem	rgenw 2681	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
⊢ φ    ⇒   ⊢ ∀x ∈ A φ
Theorem	rgen2w 2682	Generalization rule for restricted quantification. Note that x and y needn't be distinct. (Contributed by NM, 18-Jun-2014.)
⊢ φ    ⇒   ⊢ ∀x ∈ A ∀y ∈ B φ
Theorem	mprg 2683	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
⊢ (∀x ∈ A φ → ψ)    &   ⊢ (x ∈ A → φ)    ⇒   ⊢ ψ
Theorem	mprgbir 2684	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
⊢ (φ ↔ ∀x ∈ A ψ)    &   ⊢ (x ∈ A → ψ)    ⇒   ⊢ φ
Theorem	ralim 2685	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
⊢ (∀x ∈ A (φ → ψ) → (∀x ∈ A φ → ∀x ∈ A ψ))
Theorem	ralimi2 2686	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
⊢ ((x ∈ A → φ) → (x ∈ B → ψ))    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ B ψ)
Theorem	ralimia 2687	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
⊢ (x ∈ A → (φ → ψ))    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	ralimiaa 2688	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
⊢ ((x ∈ A ∧ φ) → ψ)    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	ralimi 2689	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
⊢ (φ → ψ)    ⇒   ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)
Theorem	ral2imi 2690	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (∀x ∈ A φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdaa 2691	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdva 2692*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
⊢ ((φ ∧ x ∈ A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdv 2693*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ A χ))
Theorem	ralimdv2 2694*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
⊢ (φ → ((x ∈ A → ψ) → (x ∈ B → χ)))    ⇒   ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ B χ))
Theorem	ralrimi 2695	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
⊢ Ⅎxφ    &   ⊢ (φ → (x ∈ A → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	ralrimiv 2696*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
⊢ (φ → (x ∈ A → ψ))    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	ralrimiva 2697*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
⊢ ((φ ∧ x ∈ A) → ψ)    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	ralrimivw 2698*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
⊢ (φ → ψ)    ⇒   ⊢ (φ → ∀x ∈ A ψ)
Theorem	r19.21t 2699	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)
⊢ (Ⅎxφ → (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ)))
Theorem	r19.21 2700	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by Scott Fenton, 30-Mar-2011.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ))