Theorem neleq1 3073

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∉ wnel 3067

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-nel 3068

This theorem is used by:  ruALT  9581  ssnn0fi  14041  cnpart  15317  sqrmo  15328  resqrtcl  15330  resqrtthlem  15331  sqrtneg  15344  sqreu  15438  sqrtthlem  15440  eqsqrtd  15445  ge2nprmge4  16785  prmgaplem7  17142  mgmnsgrpex  19024  sgrpnmndex  19025  iccpnfcnv  25140  griedg0prc  29651  nbgrssovtx  29748  rgrusgrprc  29976  rusgrprc  29977  rgrprcx  29979  frgrwopreglem4a  30698  xrge0iifcnv  34354  0nn0m1nnn0  35628  ppivalnnnprm  48421  fpprel  48534  gpg5nbgrvtx03star  48886  gpg5nbgr3star  48887  grlimedgnedg  48937  oddinmgm  48981