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	necomi 3001	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necomd 3002	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	nesym 3003	Characterization of inequality in terms of reversed equality (see bicom 222). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 3004	Inference associated with nesym 3003. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 3005	Inference associated with nesym 3003. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	neeq1d 3006	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 3007	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 3008	Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neeq1 3009	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 3010	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 3011	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 3012	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 3013	Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	eqnetrd 3014	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrd 3015	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	neeqtrd 3016	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetri 3017	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	eqnetrri 3018	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐵 ≠ 𝐶
Theorem	neeqtri 3019	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrri 3020	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrrd 3021	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrid 3022	A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	3netr3d 3023	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4d 3024	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐴)    &   ⊢ (𝜑 → 𝐷 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr3g 3025	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4g 3026	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	nebi 3027	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	pm13.18 3028	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 29-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	pm13.181 3029	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶)
Theorem	pm13.181OLD 3030	Obsolete version of pm13.181 3029 as of 30-Oct-2024. (Contributed by Andrew Salmon, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶)
Theorem	pm2.61ine 3031	Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝐴 = 𝐵 → 𝜑)    &   ⊢ (𝐴 ≠ 𝐵 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	pm2.21ddne 3032	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61ne 3033	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61dne 3034	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61dane 3035	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61da2ne 3036	Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)    &   ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61da3ne 3037	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓)    &   ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61iine 3038	Equality version of pm2.61ii 183. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑)    &   ⊢ (𝐴 = 𝐶 → 𝜑)    &   ⊢ (𝐵 = 𝐷 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	mteqand 3039	A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.)
⊢ (𝜑 → 𝐶 ≠ 𝐷)    &   ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neor 3040	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))
Theorem	neanior 3041	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
Theorem	ne3anior 3042	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹))
Theorem	neorian 3043	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))
Theorem	nemtbir 3044	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ ¬ 𝜑
Theorem	nelne1 3045	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	nelne2 3046	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nelelne 3047	Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV, 10-May-2020.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐴))
Theorem	neneor 3048	If two classes are different, a third class must be different of at least one of them. (Contributed by Thierry Arnoux, 8-Aug-2020.)
⊢ (𝐴 ≠ 𝐵 → (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐶))
Theorem	nfne 3049	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵
Theorem	nfned 3050	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵)
Theorem	nabbib 3051	Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) Definitial form. (Revised by Wolf Lammen, 5-Mar-2025.)
⊢ ({𝑥 ∣ 𝜑} ≠ {𝑥 ∣ 𝜓} ↔ ∃𝑥(𝜑 ↔ ¬ 𝜓))
2.1.4.2  Negated membership
Syntax	wnel 3052	Extend wff notation to include negated membership.
wff 𝐴 ∉ 𝐵
Definition	df-nel 3053	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
Theorem	neli 3054	Inference associated with df-nel 3053. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ∉ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ 𝐵
Theorem	nelir 3055	Inference associated with df-nel 3053. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∉ 𝐵
Theorem	nelcon3d 3056	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵))
Theorem	neleq12d 3057	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷))
Theorem	neleq1 3058	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))
Theorem	neleq2 3059	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵))
Theorem	nfnel 3060	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵
Theorem	nfneld 3061	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵)
Theorem	nnel 3062	Negation of negated membership, analogous to nne 2950. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	elnelne1 3063	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	elnelne2 3064	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	pm2.24nel 3065	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑))
Theorem	pm2.61danel 3066	Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.)
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
2.1.5  Restricted quantification
2.1.5.1  Restricted universal and existential quantification
Syntax	wral 3067	Extend wff notation to include restricted universal quantification.
wff ∀𝑥 ∈ 𝐴 𝜑
Definition	df-ral 3068	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. Note: This notation is most often used to express that 𝜑 holds for all elements of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather focus on those 𝑥 that happen to be contained in the corresponding 𝐴(𝑥). This hardly used interpretation could still occur naturally. For some examples, look at ralndv1 47020 or ralndv2 47021, courtesy of AV. So be careful to either keep 𝐴 independent of 𝑥, or adjust your comments to include such exotic cases. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	rgen 3069	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	ralel 3070	All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.)
⊢ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐴
Theorem	rgenw 3071	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	rgen2w 3072	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	mprg 3073	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ 𝜓
Theorem	mprgbir 3074	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜓)    ⇒   ⊢ 𝜑
Theorem	raln 3075	Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
Syntax	wrex 3076	Extend wff notation to include restricted existential quantification.
wff ∃𝑥 ∈ 𝐴 𝜑
Definition	df-rex 3077	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. Note: This notation is most often used to express that 𝜑 holds for at least one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert at least one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3068). (Contributed by NM, 30-Aug-1993.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	ralnex 3078	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	dfrex2 3079	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	nrex 3080	Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓)    ⇒   ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓
Theorem	alral 3081	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexex 3082	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)
Theorem	rextru 3083	Two ways of expressing that a class has at least one element. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ⊤)
Theorem	ralimi2 3084	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	reximi2 3085	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	ralimia 3086	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	reximia 3087	Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralimiaa 3088	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralimi 3089	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	reximi 3090	Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ral2imi 3091	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3092. (Revised by Wolf Lammen, 1-Dec-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
Theorem	ralim 3092	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
Theorem	rexim 3093	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
Theorem	reximiaOLD 3094	Obsolete version of reximia 3087 as of 31-Oct-2024. (Contributed by NM, 10-Feb-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralbii2 3095	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)
Theorem	rexbii2 3096	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)
Theorem	ralbiia 3097	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexbiia 3098	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralbii 3099	Inference adding restricted universal 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, 4-Dec-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
Theorem	rexbii 3100	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.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)