Theorem neleq1 3070

Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Assertion

Ref	Expression
neleq1	⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))

Proof of Theorem neleq1

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		eqidd 2764	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	neleq12d 3069	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∉ wnel 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-nel 3065

This theorem is referenced by:  ruALT  9572  ssnn0fi  14023  cnpart  15293  sqrmo  15304  resqrtcl  15306  resqrtthlem  15307  sqrtneg  15320  sqreu  15414  sqrtthlem  15416  eqsqrtd  15421  ge2nprmge4  16761  prmgaplem7  17118  mgmnsgrpex  18994  sgrpnmndex  18995  iccpnfcnv  25084  griedg0prc  29592  nbgrssovtx  29689  rgrusgrprc  29917  rusgrprc  29918  rgrprcx  29920  frgrwopreglem4a  30639  xrge0iifcnv  34301  0nn0m1nnn0  35582  ppivalnnnprm  48357  fpprel  48470  gpg5nbgrvtx03star  48822  gpg5nbgr3star  48823  grlimedgnedg  48873  oddinmgm  48917