Theorem neleq1 3097

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1525   ∉ wnel 3092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-clel 2865  df-nel 3093

This theorem is referenced by:  ruALT  8920  ssnn0fi  13207  cnpart  14437  sqrmo  14449  resqrtcl  14451  resqrtthlem  14452  sqrtneg  14465  sqreu  14558  sqrtthlem  14560  eqsqrtd  14565  ge2nprmge4  15878  prmgaplem7  16226  mgmnsgrpex  17861  sgrpnmndex  17862  iccpnfcnv  23235  griedg0prc  26733  nbgrssovtx  26830  rgrusgrprc  27058  rusgrprc  27059  rgrprcx  27061  frgrwopreglem4a  27777  xrge0iifcnv  30789  0nn0m1nnn0  31961  fpprel  43397  oddinmgm  43586