Theorem neleq1 3050

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∉ wnel 3044

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814  df-nel 3045

This theorem is referenced by:  ruALT  9641  ssnn0fi  14023  cnpart  15276  sqrmo  15287  resqrtcl  15289  resqrtthlem  15290  sqrtneg  15303  sqreu  15396  sqrtthlem  15398  eqsqrtd  15403  ge2nprmge4  16735  prmgaplem7  17091  mgmnsgrpex  18957  sgrpnmndex  18958  iccpnfcnv  24989  griedg0prc  29296  nbgrssovtx  29393  rgrusgrprc  29622  rusgrprc  29623  rgrprcx  29625  frgrwopreglem4a  30339  xrge0iifcnv  33894  0nn0m1nnn0  35097  fpprel  47653  gpg5nbgrvtx03star  47971  gpg5nbgr3star  47972  oddinmgm  48019