Theorem neleq1 3067

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 2761	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	neleq12d 3066	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-nel 3062

This theorem is used by:  ruALT  9606  0nn0m1nnn0  12756  ssnn0fi  14131  cnpart  15412  sqrmo  15423  resqrtcl  15425  resqrtthlem  15426  sqrtneg  15439  sqreu  15533  sqrtthlem  15535  eqsqrtd  15540  ge2nprmge4  16882  prmgaplem7  17240  mgmnsgrpex  19135  sgrpnmndex  19136  iccpnfcnv  25270  griedg0prc  29850  nbgrssovtx  29947  rgrusgrprc  30175  rusgrprc  30176  rgrprcx  30178  frgrwopreglem4a  30916  xrge0iifcnv  34611  ppivalnnnprm  48806  fpprel  48919  gpg5nbgrvtx03star  49271  gpg5nbgr3star  49272  grlimedgnedg  49322  oddinmgm  49365