Theorem neleq1 3128

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∉ wnel 3123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-nel 3124

This theorem is referenced by:  ruALT  9053  ssnn0fi  13343  cnpart  14584  sqrmo  14596  resqrtcl  14598  resqrtthlem  14599  sqrtneg  14612  sqreu  14705  sqrtthlem  14707  eqsqrtd  14712  ge2nprmge4  16028  prmgaplem7  16376  mgmnsgrpex  18079  sgrpnmndex  18080  iccpnfcnv  23531  griedg0prc  27032  nbgrssovtx  27129  rgrusgrprc  27357  rusgrprc  27358  rgrprcx  27360  frgrwopreglem4a  28073  xrge0iifcnv  31183  0nn0m1nnn0  32358  fpprel  43978  oddinmgm  44167