Theorem nelne2 3038

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)

Assertion

Ref	Expression
nelne2	⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Proof of Theorem nelne2

Step	Hyp	Ref	Expression
1		nelneq 2855	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2945	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∈ wcel 2104   ≠ wne 2938

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808  df-ne 2939

This theorem is referenced by:  nelelne  3039  elnelne2  3056  elneeldif  3961  elpwdifsn  4791  ac5num  10033  infpssrlem4  10303  fpwwe2lem12  10639  zgt1rpn0n1  13019  cats1un  14675  dprdfadd  19931  dprdcntz2  19949  lbsextlem4  20919  lindff1  21594  hauscmplem  23130  fileln0  23574  zcld  24549  dvcnvlem  25728  ppinprm  26892  chtnprm  26894  footexALT  28236  footexlem1  28237  footexlem2  28238  foot  28240  colperpexlem3  28250  mideulem2  28252  opphllem  28253  opphllem2  28266  lnopp2hpgb  28281  colhp  28288  lmieu  28302  trgcopy  28322  trgcopyeulem  28323  cycpmco2lem1  32555  cycpmco2  32562  cyc3genpmlem  32580  linds2eq  32771  elrspunsn  32821  mxidlnzr  32857  lindsunlem  32997  fedgmul  33004  extdg1id  33030  ordtconnlem1  33202  esum2dlem  33388  subfacp1lem5  34473  heiborlem6  36987  llnle  38692  lplnle  38714  lhpexle1lem  39181  cdleme18b  39466  cdlemg46  39909  cdlemh  39991  bcc0  43401  fnchoice  44015  climxrre  44764  stoweidlem43  45057  zneoALTV  46635