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	necon4bid 3001	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
Theorem	necon3abii 3002	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 3003	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon1abii 3004	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)
Theorem	necon1bbii 3005	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)
Theorem	necon2abii 3006	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon2bbii 3007	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bii 3008	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necom 3009	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
Theorem	necomi 3010	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necomd 3011	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	nesym 3012	Characterization of inequality in terms of reversed equality (see bicom 224). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 3013	Inference associated with nesym 3012. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 3014	Inference associated with nesym 3012. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	neeq1d 3015	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 3016	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 3017	Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neeq1 3018	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 3019	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 3020	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 3021	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 3022	Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	eqnetrd 3023	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrd 3024	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	neeqtrd 3025	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetri 3026	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	eqnetrri 3027	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐵 ≠ 𝐶
Theorem	neeqtri 3028	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrri 3029	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrrd 3030	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrid 3031	A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	3netr3d 3032	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 3033	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 3034	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4g 3035	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	nebi 3036	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	pm13.18 3037	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 3038	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Oct-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶)
Theorem	pm2.61ine 3039	Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝐴 = 𝐵 → 𝜑)    &   ⊢ (𝐴 ≠ 𝐵 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	pm2.21ddne 3040	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61ne 3041	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 3042	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61dane 3043	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61da2ne 3044	Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)    &   ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61da3ne 3045	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓)    &   ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61iine 3046	Equality version of pm2.61ii 184. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑)    &   ⊢ (𝐴 = 𝐶 → 𝜑)    &   ⊢ (𝐵 = 𝐷 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	mteqand 3047	A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.)
⊢ (𝜑 → 𝐶 ≠ 𝐷)    &   ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	neor 3048	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))
Theorem	neanior 3049	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
Theorem	ne3anior 3050	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹))
Theorem	neorian 3051	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))
Theorem	nemtbir 3052	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ ¬ 𝜑
Theorem	nelne1 3053	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 3054	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 3055	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 3056	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 3057	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵
Theorem	nfned 3058	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵)
Theorem	nabbib 3059	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 3060	Extend wff notation to include negated membership.
wff 𝐴 ∉ 𝐵
Definition	df-nel 3061	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
Theorem	neli 3062	Inference associated with df-nel 3061. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ∉ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ 𝐵
Theorem	nelir 3063	Inference associated with df-nel 3061. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∉ 𝐵
Theorem	nelcon3d 3064	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵))
Theorem	neleq12d 3065	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷))
Theorem	neleq1 3066	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))
Theorem	neleq2 3067	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵))
Theorem	nfnel 3068	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵
Theorem	nfneld 3069	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵)
Theorem	nnel 3070	Negation of negated membership, analogous to nne 2960. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	elnelne1 3071	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	elnelne2 3072	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	pm2.24nel 3073	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑))
Theorem	pm2.61danel 3074	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 3075	Extend wff notation to include restricted universal quantification.
wff ∀𝑥 ∈ 𝐴 𝜑
Definition	df-ral 3076	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 47663 or ralndv2 47664, 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 3077	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	ralel 3078	All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.)
⊢ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐴
Theorem	rgenw 3079	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 𝜑
Theorem	rgen2w 3080	Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑
Theorem	mprg 3081	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜑)    ⇒   ⊢ 𝜓
Theorem	mprgbir 3082	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝑥 ∈ 𝐴 → 𝜓)    ⇒   ⊢ 𝜑
Theorem	ralrid 3083	Sufficient condition for the restricted universal quantifier. Deduction form. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	raln 3084	Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
Syntax	wrex 3085	Extend wff notation to include restricted existential quantification.
wff ∃𝑥 ∈ 𝐴 𝜑
Definition	df-rex 3086	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 3076). (Contributed by NM, 30-Aug-1993.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	ralnex 3087	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	dfrex2 3088	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	nrex 3089	Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓)    ⇒   ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓
Theorem	alral 3090	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexex 3091	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)
Theorem	rextru 3092	Two ways of expressing that a class has at least one element. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ⊤)
Theorem	ralimi2 3093	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
Theorem	reximi2 3094	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	ralimia 3095	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	reximia 3096	Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralimiaa 3097	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	ralimi 3098	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
Theorem	reximi 3099	Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ral2imi 3100	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3101. (Revised by Wolf Lammen, 1-Dec-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))