Theorem neleq1 3052

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-nel 3047

This theorem is referenced by:  ruALT  9643  ssnn0fi  14026  cnpart  15279  sqrmo  15290  resqrtcl  15292  resqrtthlem  15293  sqrtneg  15306  sqreu  15399  sqrtthlem  15401  eqsqrtd  15406  ge2nprmge4  16738  prmgaplem7  17095  mgmnsgrpex  18944  sgrpnmndex  18945  iccpnfcnv  24975  griedg0prc  29281  nbgrssovtx  29378  rgrusgrprc  29607  rusgrprc  29608  rgrprcx  29610  frgrwopreglem4a  30329  xrge0iifcnv  33932  0nn0m1nnn0  35118  fpprel  47715  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  oddinmgm  48091