Theorem neleq1 3069

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∉ wnel 3063

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-nel 3064

This theorem is used by:  ruALT  9585  0nn0m1nnn0  12679  ssnn0fi  14053  cnpart  15331  sqrmo  15342  resqrtcl  15344  resqrtthlem  15345  sqrtneg  15358  sqreu  15452  sqrtthlem  15454  eqsqrtd  15459  ge2nprmge4  16798  prmgaplem7  17155  mgmnsgrpex  19049  sgrpnmndex  19050  iccpnfcnv  25178  griedg0prc  29732  nbgrssovtx  29829  rgrusgrprc  30057  rusgrprc  30058  rgrprcx  30060  frgrwopreglem4a  30798  xrge0iifcnv  34451  ppivalnnnprm  48539  fpprel  48652  gpg5nbgrvtx03star  49004  gpg5nbgr3star  49005  grlimedgnedg  49055  oddinmgm  49098