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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-nel 3037

This theorem is referenced by:  ruALT  9511  ssnn0fi  13908  cnpart  15163  sqrmo  15174  resqrtcl  15176  resqrtthlem  15177  sqrtneg  15190  sqreu  15284  sqrtthlem  15286  eqsqrtd  15291  ge2nprmge4  16628  prmgaplem7  16985  mgmnsgrpex  18856  sgrpnmndex  18857  iccpnfcnv  24898  griedg0prc  29337  nbgrssovtx  29434  rgrusgrprc  29663  rusgrprc  29664  rgrprcx  29666  frgrwopreglem4a  30385  xrge0iifcnv  34090  0nn0m1nnn0  35307  fpprel  47970  gpg5nbgrvtx03star  48322  gpg5nbgr3star  48323  grlimedgnedg  48373  oddinmgm  48417