Theorem neleq1 3035

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∉ wnel 3029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-nel 3030

This theorem is referenced by:  ruALT  9517  ssnn0fi  13910  cnpart  15165  sqrmo  15176  resqrtcl  15178  resqrtthlem  15179  sqrtneg  15192  sqreu  15286  sqrtthlem  15288  eqsqrtd  15293  ge2nprmge4  16630  prmgaplem7  16987  mgmnsgrpex  18823  sgrpnmndex  18824  iccpnfcnv  24858  griedg0prc  29227  nbgrssovtx  29324  rgrusgrprc  29553  rusgrprc  29554  rgrprcx  29556  frgrwopreglem4a  30272  xrge0iifcnv  33899  0nn0m1nnn0  35085  fpprel  47713  gpg5nbgrvtx03star  48065  gpg5nbgr3star  48066  grlimedgnedg  48116  oddinmgm  48160