Theorem neleq1 3036

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-nel 3031

This theorem is referenced by:  ruALT  9563  ssnn0fi  13957  cnpart  15213  sqrmo  15224  resqrtcl  15226  resqrtthlem  15227  sqrtneg  15240  sqreu  15334  sqrtthlem  15336  eqsqrtd  15341  ge2nprmge4  16678  prmgaplem7  17035  mgmnsgrpex  18865  sgrpnmndex  18866  iccpnfcnv  24849  griedg0prc  29198  nbgrssovtx  29295  rgrusgrprc  29524  rusgrprc  29525  rgrprcx  29527  frgrwopreglem4a  30246  xrge0iifcnv  33930  0nn0m1nnn0  35107  fpprel  47733  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  oddinmgm  48167