Theorem neleq1 3042

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∉ wnel 3036

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-nel 3037

This theorem is referenced by:  ruALT  9617  ssnn0fi  14003  cnpart  15259  sqrmo  15270  resqrtcl  15272  resqrtthlem  15273  sqrtneg  15286  sqreu  15379  sqrtthlem  15381  eqsqrtd  15386  ge2nprmge4  16720  prmgaplem7  17077  mgmnsgrpex  18909  sgrpnmndex  18910  iccpnfcnv  24893  griedg0prc  29243  nbgrssovtx  29340  rgrusgrprc  29569  rusgrprc  29570  rgrprcx  29572  frgrwopreglem4a  30291  xrge0iifcnv  33964  0nn0m1nnn0  35135  fpprel  47742  gpg5nbgrvtx03star  48082  gpg5nbgr3star  48083  oddinmgm  48150