Theorem nelne2 3031

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 2861	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2940	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-ne 2934

This theorem is referenced by:  nelelne  3032  elnelne2  3049  elneeldif  3916  elpwdifsn  4746  f1ounsn  7220  ac5num  9950  infpssrlem4  10220  fpwwe2lem12  10557  zgt1rpn0n1  12952  cats1un  14648  dprdfadd  19955  dprdcntz2  19973  lbsextlem4  21120  lindff1  21779  hauscmplem  23354  fileln0  23798  zcld  24762  dvcnvlem  25940  ppinprm  27122  chtnprm  27124  footexALT  28794  footexlem1  28795  footexlem2  28796  foot  28798  colperpexlem3  28808  mideulem2  28810  opphllem  28811  opphllem2  28824  lnopp2hpgb  28839  colhp  28846  lmieu  28860  trgcopy  28880  trgcopyeulem  28881  cycpmco2lem1  33210  cycpmco2  33217  cyc3genpmlem  33235  unitnz  33323  fracfld  33392  linds2eq  33464  elrspunsn  33512  mxidlnzr  33550  lindsunlem  33783  fedgmul  33790  extdg1id  33825  2sqr3minply  33939  cos9thpiminplylem2  33942  ordtconnlem1  34083  esum2dlem  34251  subfacp1lem5  35380  heiborlem6  38019  llnle  39846  lplnle  39868  lhpexle1lem  40335  cdleme18b  40620  cdlemg46  41063  cdlemh  41145  ine1  42636  bcc0  44648  fnchoice  45341  climxrre  46061  stoweidlem43  46354  zneoALTV  47982  oppfrcllem  49439  oppfrcl2  49441  eloppf  49445