Theorem neleq1 3042

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∉ wnel 3036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803  df-nel 3037

This theorem is referenced by:  ruALT  9646  ssnn0fi  14005  cnpart  15245  sqrmo  15256  resqrtcl  15258  resqrtthlem  15259  sqrtneg  15272  sqreu  15365  sqrtthlem  15367  eqsqrtd  15372  ge2nprmge4  16702  prmgaplem7  17059  mgmnsgrpex  18921  sgrpnmndex  18922  iccpnfcnv  24960  griedg0prc  29200  nbgrssovtx  29297  rgrusgrprc  29526  rusgrprc  29527  rgrprcx  29529  frgrwopreglem4a  30243  xrge0iifcnv  33748  0nn0m1nnn0  34940  fpprel  47300  oddinmgm  47552