Theorem neleq1 3058

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∉ wnel 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-nel 3053

This theorem is referenced by:  ruALT  9672  ssnn0fi  14036  cnpart  15289  sqrmo  15300  resqrtcl  15302  resqrtthlem  15303  sqrtneg  15316  sqreu  15409  sqrtthlem  15411  eqsqrtd  15416  ge2nprmge4  16748  prmgaplem7  17104  mgmnsgrpex  18966  sgrpnmndex  18967  iccpnfcnv  24994  griedg0prc  29299  nbgrssovtx  29396  rgrusgrprc  29625  rusgrprc  29626  rgrprcx  29628  frgrwopreglem4a  30342  xrge0iifcnv  33879  0nn0m1nnn0  35080  fpprel  47602  oddinmgm  47898