Theorem neleq1 2902

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∉ wnel 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-nel 2898

This theorem is referenced by:  ruALT  8508  ssnn0fi  12784  cnpart  13980  sqrmo  13992  resqrtcl  13994  resqrtthlem  13995  sqrtneg  14008  sqreu  14100  sqrtthlem  14102  eqsqrtd  14107  prmgaplem7  15761  mgmnsgrpex  17418  sgrpnmndex  17419  iccpnfcnv  22743  griedg0prc  26156  nbgrssovtx  26260  rgrusgrprc  26485  rusgrprc  26486  rgrprcx  26488  frgrwopreglem4a  27174  xrge0iifcnv  29979  oddinmgm  41815