Theorem neleq1 3128

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∉ wnel 3123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-nel 3124

This theorem is referenced by:  ruALT  9061  ssnn0fi  13347  cnpart  14593  sqrmo  14605  resqrtcl  14607  resqrtthlem  14608  sqrtneg  14621  sqreu  14714  sqrtthlem  14716  eqsqrtd  14721  ge2nprmge4  16039  prmgaplem7  16387  mgmnsgrpex  18090  sgrpnmndex  18091  iccpnfcnv  23542  griedg0prc  27040  nbgrssovtx  27137  rgrusgrprc  27365  rusgrprc  27366  rgrprcx  27368  frgrwopreglem4a  28083  xrge0iifcnv  31171  0nn0m1nnn0  32346  fpprel  43887  oddinmgm  44076