Theorem nelne2 3058

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-ne 2961

This theorem is used by:  nelelne  3061  elnelne2  3078  elneeldif  3920  elpwdifsn  4759  f1ounsn  7279  ac5num  10036  infpssrlem4  10305  fpwwe2lem12  10646  zgt1rpn0n1  13079  cats1un  14784  dprdfadd  20140  dprdcntz2  20158  lbsextlem4  21339  lindff1  22024  hauscmplem  23617  fileln0  24062  zcld  25026  dvcnvlem  26190  ppinprm  27371  chtnprm  27373  tglnpt4  28983  footexALT  29053  footexlem1  29054  footexlem2  29055  foot  29057  colperpexlem3  29068  mideulem2  29070  opphllem  29071  opphllem2  29084  lnopp2hpgb  29100  colhp  29107  plngrotlem1  29124  plngrotlem2  29125  plngrot  29127  lnssplnglem  29128  lmieu  29148  trgcopy  29170  trgcopyeulem  29171  ragraghl  29204  tgaaddcpbllem1  29207  tgaaddcpbl  29210  perpprlng  29259  prlngex  29260  prlngmolem1  29261  prlngmid2  29270  quadcgrprlng  29275  cycpmco2lem1  33514  cycpmco2  33521  cyc3genpmlem  33539  unitnz  33626  fracfld  33697  linds2eq  33762  elrspunsn  33805  mxidlnzr  33818  lindsunlem  34082  fedgmul  34089  extdg1id  34124  2sqr3minply  34238  cos9thpiminplylem2  34241  ordtconnlem1  34382  esum2dlem  34550  subfacp1lem5  35717  mh-inf3f1  37113  heiborlem6  38529  llnle  40354  lplnle  40376  lhpexle1lem  40843  cdleme18b  41128  cdlemg46  41571  cdlemh  41653  ine1  43152  bcc0  45127  fnchoice  45826  climxrre  46541  stoweidlem43  46834  zneoALTV  48511  oppfrcllem  49981  oppfrcl2  49983  eloppf  49987