Theorem neleq1 3054

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∉ wnel 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-nel 3050

This theorem is referenced by:  ruALT  9362  ssnn0fi  13705  cnpart  14951  sqrmo  14963  resqrtcl  14965  resqrtthlem  14966  sqrtneg  14979  sqreu  15072  sqrtthlem  15074  eqsqrtd  15079  ge2nprmge4  16406  prmgaplem7  16758  mgmnsgrpex  18570  sgrpnmndex  18571  iccpnfcnv  24107  griedg0prc  27631  nbgrssovtx  27728  rgrusgrprc  27956  rusgrprc  27957  rgrprcx  27959  frgrwopreglem4a  28674  xrge0iifcnv  31883  0nn0m1nnn0  33071  fpprel  45180  oddinmgm  45369