Theorem neleq1 3067

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∉ wnel 3061

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-nel 3062

This theorem is used by:  ruALT  9581  0nn0m1nnn0  12675  ssnn0fi  14049  cnpart  15327  sqrmo  15338  resqrtcl  15340  resqrtthlem  15341  sqrtneg  15354  sqreu  15448  sqrtthlem  15450  eqsqrtd  15455  ge2nprmge4  16792  prmgaplem7  17149  mgmnsgrpex  19043  sgrpnmndex  19044  iccpnfcnv  25172  griedg0prc  29724  nbgrssovtx  29821  rgrusgrprc  30049  rusgrprc  30050  rgrprcx  30052  frgrwopreglem4a  30790  xrge0iifcnv  34443  ppivalnnnprm  48531  fpprel  48644  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  grlimedgnedg  49047  oddinmgm  49090