Theorem neleq1 3071

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 3070	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∉ wnel 3065

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-nel 3066

This theorem is used by:  ruALT  9630  0nn0m1nnn0  12780  ssnn0fi  14155  cnpart  15436  sqrmo  15447  resqrtcl  15449  resqrtthlem  15450  sqrtneg  15463  sqreu  15557  sqrtthlem  15559  eqsqrtd  15564  ge2nprmge4  16906  prmgaplem7  17264  mgmnsgrpex  19159  sgrpnmndex  19160  iccpnfcnv  25295  griedg0prc  29875  nbgrssovtx  29972  rgrusgrprc  30200  rusgrprc  30201  rgrprcx  30203  frgrwopreglem4a  30941  xrge0iifcnv  34635  ppivalnnnprm  48918  fpprel  49031  gpg5nbgrvtx03star  49383  gpg5nbgr3star  49384  grlimedgnedg  49434  oddinmgm  49477