Theorem neleq1 3045

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∉ wnel 3039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815  df-nel 3040

This theorem is referenced by:  ruALT  9521  ssnn0fi  13945  cnpart  15200  sqrmo  15211  resqrtcl  15213  resqrtthlem  15214  sqrtneg  15227  sqreu  15321  sqrtthlem  15323  eqsqrtd  15328  ge2nprmge4  16669  prmgaplem7  17026  mgmnsgrpex  18900  sgrpnmndex  18901  iccpnfcnv  24936  griedg0prc  29358  nbgrssovtx  29455  rgrusgrprc  29683  rusgrprc  29684  rgrprcx  29686  frgrwopreglem4a  30405  xrge0iifcnv  34124  0nn0m1nnn0  35348  ppivalnnnprm  48113  fpprel  48226  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  grlimedgnedg  48629  oddinmgm  48673