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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∉ wnel 3046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729  df-clel 2816  df-nel 3047

This theorem is referenced by:  ruALT  9219  ssnn0fi  13558  cnpart  14803  sqrmo  14815  resqrtcl  14817  resqrtthlem  14818  sqrtneg  14831  sqreu  14924  sqrtthlem  14926  eqsqrtd  14931  ge2nprmge4  16258  prmgaplem7  16610  mgmnsgrpex  18358  sgrpnmndex  18359  iccpnfcnv  23841  griedg0prc  27352  nbgrssovtx  27449  rgrusgrprc  27677  rusgrprc  27678  rgrprcx  27680  frgrwopreglem4a  28393  xrge0iifcnv  31597  0nn0m1nnn0  32784  fpprel  44853  oddinmgm  45042