Theorem nelne2 3024

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

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

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-ne 2927

This theorem is referenced by:  nelelne  3025  elnelne2  3042  elneeldif  3931  elpwdifsn  4756  f1ounsn  7250  ac5num  9996  infpssrlem4  10266  fpwwe2lem12  10602  zgt1rpn0n1  13001  cats1un  14693  dprdfadd  19959  dprdcntz2  19977  lbsextlem4  21078  lindff1  21736  hauscmplem  23300  fileln0  23744  zcld  24709  dvcnvlem  25887  ppinprm  27069  chtnprm  27071  footexALT  28652  footexlem1  28653  footexlem2  28654  foot  28656  colperpexlem3  28666  mideulem2  28668  opphllem  28669  opphllem2  28682  lnopp2hpgb  28697  colhp  28704  lmieu  28718  trgcopy  28738  trgcopyeulem  28739  cycpmco2lem1  33090  cycpmco2  33097  cyc3genpmlem  33115  unitnz  33197  fracfld  33265  linds2eq  33359  elrspunsn  33407  mxidlnzr  33445  lindsunlem  33627  fedgmul  33634  extdg1id  33668  2sqr3minply  33777  cos9thpiminplylem2  33780  ordtconnlem1  33921  esum2dlem  34089  subfacp1lem5  35178  heiborlem6  37817  llnle  39519  lplnle  39541  lhpexle1lem  40008  cdleme18b  40293  cdlemg46  40736  cdlemh  40818  ine1  42309  bcc0  44336  fnchoice  45030  climxrre  45755  stoweidlem43  46048  zneoALTV  47674  oppfrcllem  49120  oppfrcl2  49122  eloppf  49126