Theorem neleq1 3053

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 3052	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-nel 3049

This theorem is referenced by:  ruALT  9292  ssnn0fi  13633  cnpart  14879  sqrmo  14891  resqrtcl  14893  resqrtthlem  14894  sqrtneg  14907  sqreu  15000  sqrtthlem  15002  eqsqrtd  15007  ge2nprmge4  16334  prmgaplem7  16686  mgmnsgrpex  18485  sgrpnmndex  18486  iccpnfcnv  24013  griedg0prc  27534  nbgrssovtx  27631  rgrusgrprc  27859  rusgrprc  27860  rgrprcx  27862  frgrwopreglem4a  28575  xrge0iifcnv  31785  0nn0m1nnn0  32971  fpprel  45068  oddinmgm  45257