Theorem neleq1 3042

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∉ wnel 3036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-nel 3037

This theorem is referenced by:  ruALT  9523  ssnn0fi  13947  cnpart  15202  sqrmo  15213  resqrtcl  15215  resqrtthlem  15216  sqrtneg  15229  sqreu  15323  sqrtthlem  15325  eqsqrtd  15330  ge2nprmge4  16671  prmgaplem7  17028  mgmnsgrpex  18902  sgrpnmndex  18903  iccpnfcnv  24911  griedg0prc  29333  nbgrssovtx  29430  rgrusgrprc  29658  rusgrprc  29659  rgrprcx  29661  frgrwopreglem4a  30380  xrge0iifcnv  34077  0nn0m1nnn0  35295  ppivalnnnprm  48091  fpprel  48204  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  grlimedgnedg  48607  oddinmgm  48651