Theorem neleq1 3053

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∉ wnel 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-nel 3048

This theorem is referenced by:  ruALT  9598  ssnn0fi  13950  cnpart  15187  sqrmo  15198  resqrtcl  15200  resqrtthlem  15201  sqrtneg  15214  sqreu  15307  sqrtthlem  15309  eqsqrtd  15314  ge2nprmge4  16638  prmgaplem7  16990  mgmnsgrpex  18812  sgrpnmndex  18813  iccpnfcnv  24460  griedg0prc  28521  nbgrssovtx  28618  rgrusgrprc  28846  rusgrprc  28847  rgrprcx  28849  frgrwopreglem4a  29563  xrge0iifcnv  32913  0nn0m1nnn0  34102  fpprel  46396  oddinmgm  46585