Theorem neleq1 3068

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-nel 3063

This theorem is used by:  ruALT  9587  0nn0m1nnn0  12734  ssnn0fi  14108  cnpart  15387  sqrmo  15398  resqrtcl  15400  resqrtthlem  15401  sqrtneg  15414  sqreu  15508  sqrtthlem  15510  eqsqrtd  15515  ge2nprmge4  16857  prmgaplem7  17215  mgmnsgrpex  19110  sgrpnmndex  19111  iccpnfcnv  25245  griedg0prc  29827  nbgrssovtx  29924  rgrusgrprc  30152  rusgrprc  30153  rgrprcx  30155  frgrwopreglem4a  30893  xrge0iifcnv  34547  ppivalnnnprm  48657  fpprel  48770  gpg5nbgrvtx03star  49122  gpg5nbgr3star  49123  grlimedgnedg  49173  oddinmgm  49216