Theorem neleq1 3051

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∉ wnel 3046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728  df-clel 2814  df-nel 3047

This theorem is referenced by:  ruALT  9461  ssnn0fi  13807  cnpart  15051  sqrmo  15063  resqrtcl  15065  resqrtthlem  15066  sqrtneg  15079  sqreu  15172  sqrtthlem  15174  eqsqrtd  15179  ge2nprmge4  16504  prmgaplem7  16856  mgmnsgrpex  18667  sgrpnmndex  18668  iccpnfcnv  24214  griedg0prc  27921  nbgrssovtx  28018  rgrusgrprc  28246  rusgrprc  28247  rgrprcx  28249  frgrwopreglem4a  28963  xrge0iifcnv  32181  0nn0m1nnn0  33370  fpprel  45598  oddinmgm  45787