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  9556  ssnn0fi  13950  cnpart  15206  sqrmo  15217  resqrtcl  15219  resqrtthlem  15220  sqrtneg  15233  sqreu  15327  sqrtthlem  15329  eqsqrtd  15334  ge2nprmge4  16671  prmgaplem7  17028  mgmnsgrpex  18858  sgrpnmndex  18859  iccpnfcnv  24842  griedg0prc  29191  nbgrssovtx  29288  rgrusgrprc  29517  rusgrprc  29518  rgrprcx  29520  frgrwopreglem4a  30239  xrge0iifcnv  33923  0nn0m1nnn0  35100  fpprel  47729  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  oddinmgm  48163