Theorem neleq1 3039

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∉ wnel 3033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-nel 3034

This theorem is referenced by:  ruALT  9499  ssnn0fi  13894  cnpart  15149  sqrmo  15160  resqrtcl  15162  resqrtthlem  15163  sqrtneg  15176  sqreu  15270  sqrtthlem  15272  eqsqrtd  15277  ge2nprmge4  16614  prmgaplem7  16971  mgmnsgrpex  18841  sgrpnmndex  18842  iccpnfcnv  24870  griedg0prc  29244  nbgrssovtx  29341  rgrusgrprc  29570  rusgrprc  29571  rgrprcx  29573  frgrwopreglem4a  30292  xrge0iifcnv  33967  0nn0m1nnn0  35178  fpprel  47852  gpg5nbgrvtx03star  48204  gpg5nbgr3star  48205  grlimedgnedg  48255  oddinmgm  48299