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	necon3i 3001	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon1i 3002	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)
Theorem	necon2i 3003	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)
Theorem	necon4i 3004	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → 𝐴 = 𝐵)
Theorem	necon3abid 3005	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bbid 3006	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon1abid 3007	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓))
Theorem	necon1bbid 3008	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 = 𝐵))
Theorem	necon4abid 3009	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
Theorem	necon4bbid 3010	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))
Theorem	necon2abid 3011	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))
Theorem	necon2bbid 3012	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Theorem	necon3bid 3013	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	necon4bid 3014	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
Theorem	necon3abii 3015	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (𝐴 = 𝐵 ↔ 𝜑)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bbii 3016	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon1abii 3017	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)
Theorem	necon1bbii 3018	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝜑)    ⇒   ⊢ (¬ 𝜑 ↔ 𝐴 = 𝐵)
Theorem	necon2abii 3019	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)
Theorem	necon2bbii 3020	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (𝜑 ↔ 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ¬ 𝜑)
Theorem	necon3bii 3021	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)    ⇒   ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)
Theorem	necom 3022	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
Theorem	necomi 3023	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	necomd 3024	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐴)
Theorem	nesym 3025	Characterization of inequality in terms of reversed equality (see bicom 214). (Contributed by BJ, 7-Jul-2018.)
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)
Theorem	nesymi 3026	Inference associated with nesym 3025. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 ≠ 𝐵    ⇒   ⊢ ¬ 𝐵 = 𝐴
Theorem	nesymir 3027	Inference associated with nesym 3025. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ¬ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 ≠ 𝐴
Theorem	neeq1d 3028	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2d 3029	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq12d 3030	Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))
Theorem	neeq1 3031	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
Theorem	neeq2 3032	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
Theorem	neeq1i 3033	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
Theorem	neeq2i 3034	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)
Theorem	neeq12i 3035	Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)
Theorem	eqnetrd 3036	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetrrd 3037	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 𝐶)
Theorem	neeqtrd 3038	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	eqnetri 3039	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 ≠ 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	eqnetrri 3040	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ 𝐵 ≠ 𝐶
Theorem	neeqtri 3041	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrri 3042	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐶 = 𝐵    ⇒   ⊢ 𝐴 ≠ 𝐶
Theorem	neeqtrrd 3043	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	syl5eqner 3044	A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
⊢ 𝐵 = 𝐴    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐶)
Theorem	3netr3d 3045	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 3046	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 3047	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐴 = 𝐶    &   ⊢ 𝐵 = 𝐷    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	3netr4g 3048	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ 𝐶 = 𝐴    &   ⊢ 𝐷 = 𝐵    ⇒   ⊢ (𝜑 → 𝐶 ≠ 𝐷)
Theorem	nebi 3049	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
Theorem	pm13.18 3050	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 14-May-2023.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	pm13.18OLD 3051	Obsolete version of pm13.18 3050 as of 14-May-2023. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	pm13.181 3052	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶)
Theorem	pm2.61ine 3053	Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝐴 = 𝐵 → 𝜑)    &   ⊢ (𝐴 ≠ 𝐵 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	pm2.21ddne 3054	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61ne 3055	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 3056	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61dane 3057	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61da2ne 3058	Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)    &   ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61da3ne 3059	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓)    &   ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	pm2.61iine 3060	Equality version of pm2.61ii 178. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑)    &   ⊢ (𝐴 = 𝐶 → 𝜑)    &   ⊢ (𝐵 = 𝐷 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	neor 3061	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))
Theorem	neanior 3062	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
Theorem	ne3anior 3063	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹))
Theorem	neorian 3064	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))
Theorem	nemtbir 3065	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ (𝜑 ↔ 𝐴 = 𝐵)    ⇒   ⊢ ¬ 𝜑
Theorem	nelne1 3066	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	nelne1OLD 3067	Obsolete version of nelne1 3066 asw of 14-May-2023. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	nelne2 3068	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	nelne2OLD 3069	Obsolete version of nelne2 3068 asw of 14-May-2023. (Contributed by NM, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nelelne 3070	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 3071	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 3072	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵
Theorem	nfned 3073	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵)
Theorem	nabbi 3074	Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (∃𝑥(𝜑 ↔ ¬ 𝜓) ↔ {𝑥 ∣ 𝜑} ≠ {𝑥 ∣ 𝜓})
2.1.4.2  Negated membership
Syntax	wnel 3075	Extend wff notation to include negated membership.
wff 𝐴 ∉ 𝐵
Definition	df-nel 3076	Define negated membership. (Contributed by NM, 7-Aug-1994.)
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
Theorem	neli 3077	Inference associated with df-nel 3076. (Contributed by BJ, 7-Jul-2018.)
⊢ 𝐴 ∉ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ 𝐵
Theorem	nelir 3078	Inference associated with df-nel 3076. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∉ 𝐵
Theorem	neleq12d 3079	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷))
Theorem	neleq1 3080	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))
Theorem	neleq2 3081	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵))
Theorem	nfnel 3082	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵
Theorem	nfneld 3083	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝐵)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵)
Theorem	nnel 3084	Negation of negated membership, analogous to nne 2973. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	elnelne1 3085	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶)
Theorem	elnelne2 3086	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵)
Theorem	nelcon3d 3087	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷))    ⇒   ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵))
Theorem	elnelall 3088	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑))
Theorem	pm2.61danel 3089	Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.)
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
2.1.5  Restricted quantification
Syntax	wral 3090	Extend wff notation to include restricted universal quantification.
wff ∀𝑥 ∈ 𝐴 𝜑
Syntax	wrex 3091	Extend wff notation to include restricted existential quantification.
wff ∃𝑥 ∈ 𝐴 𝜑
Syntax	wreu 3092	Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥 ∈ 𝐴 𝜑
Syntax	wrmo 3093	Extend wff notation to include restricted "at most one."
wff ∃*𝑥 ∈ 𝐴 𝜑
Syntax	crab 3094	Extend class notation to include the restricted class abstraction (class builder).
class {𝑥 ∈ 𝐴 ∣ 𝜑}
Definition	df-ral 3095	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Definition	df-rex 3096	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-reu 3097	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-rmo 3098	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Definition	df-rab 3099	Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
Theorem	ralanid 3100	Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.)
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑)