Theorem neleq1 3070

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∉ wnel 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840  df-nel 3065

This theorem is referenced by:  ruALT  9559  ssnn0fi  14012  cnpart  15281  sqrmo  15292  resqrtcl  15294  resqrtthlem  15295  sqrtneg  15308  sqreu  15402  sqrtthlem  15404  eqsqrtd  15409  ge2nprmge4  16750  prmgaplem7  17107  mgmnsgrpex  18983  sgrpnmndex  18984  iccpnfcnv  25064  griedg0prc  29523  nbgrssovtx  29620  rgrusgrprc  29848  rusgrprc  29849  rgrprcx  29851  frgrwopreglem4a  30570  xrge0iifcnv  34240  0nn0m1nnn0  35475  ppivalnnnprm  48235  fpprel  48348  gpg5nbgrvtx03star  48700  gpg5nbgr3star  48701  grlimedgnedg  48751  oddinmgm  48795