Theorem neleq1 3066

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∉ wnel 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-nel 3061

This theorem is referenced by:  ruALT  9554  ssnn0fi  13995  cnpart  15250  sqrmo  15261  resqrtcl  15263  resqrtthlem  15264  sqrtneg  15277  sqreu  15371  sqrtthlem  15373  eqsqrtd  15378  ge2nprmge4  16719  prmgaplem7  17076  mgmnsgrpex  18951  sgrpnmndex  18952  iccpnfcnv  24986  griedg0prc  29411  nbgrssovtx  29508  rgrusgrprc  29736  rusgrprc  29737  rgrprcx  29739  frgrwopreglem4a  30458  xrge0iifcnv  34191  0nn0m1nnn0  35427  ppivalnnnprm  48201  fpprel  48314  gpg5nbgrvtx03star  48666  gpg5nbgr3star  48667  grlimedgnedg  48717  oddinmgm  48761