Theorem neleq1 3035

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∉ wnel 3029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-nel 3030

This theorem is referenced by:  ruALT  9498  ssnn0fi  13892  cnpart  15147  sqrmo  15158  resqrtcl  15160  resqrtthlem  15161  sqrtneg  15174  sqreu  15268  sqrtthlem  15270  eqsqrtd  15275  ge2nprmge4  16612  prmgaplem7  16969  mgmnsgrpex  18805  sgrpnmndex  18806  iccpnfcnv  24840  griedg0prc  29213  nbgrssovtx  29310  rgrusgrprc  29539  rusgrprc  29540  rgrprcx  29542  frgrwopreglem4a  30258  xrge0iifcnv  33916  0nn0m1nnn0  35106  fpprel  47732  gpg5nbgrvtx03star  48084  gpg5nbgr3star  48085  grlimedgnedg  48135  oddinmgm  48179