Theorem nelne2 3062

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-ne 2965

This theorem is referenced by:  nelelne  3065  elnelne2  3082  elneeldif  3927  elpwdifsn  4761  f1ounsn  7273  ac5num  10022  infpssrlem4  10292  fpwwe2lem12  10629  zgt1rpn0n1  13061  cats1un  14760  dprdfadd  20094  dprdcntz2  20112  lbsextlem4  21265  lindff1  21941  hauscmplem  23534  fileln0  23978  zcld  24942  dvcnvlem  26106  ppinprm  27284  chtnprm  27286  tglnpt4  28892  footexALT  28959  footexlem1  28960  footexlem2  28961  foot  28963  colperpexlem3  28974  mideulem2  28976  opphllem  28977  opphllem2  28990  lnopp2hpgb  29006  colhp  29013  plngrotlem1  29029  plngrotlem2  29030  plngrot  29032  lnssplnglem  29033  lmieu  29053  trgcopy  29074  trgcopyeulem  29075  ragraghl  29106  perpprlng  29155  prlngex  29156  prlngmolem1  29157  cycpmco2lem1  33389  cycpmco2  33396  cyc3genpmlem  33414  unitnz  33501  fracfld  33574  linds2eq  33640  elrspunsn  33683  mxidlnzr  33697  lindsunlem  33961  fedgmul  33968  extdg1id  34003  2sqr3minply  34117  cos9thpiminplylem2  34120  ordtconnlem1  34261  esum2dlem  34429  subfacp1lem5  35611  mh-inf3f1  36977  heiborlem6  38392  llnle  40219  lplnle  40241  lhpexle1lem  40708  cdleme18b  40993  cdlemg46  41436  cdlemh  41518  ine1  43002  bcc0  44979  fnchoice  45678  climxrre  46393  stoweidlem43  46686  zneoALTV  48360  oppfrcllem  49827  oppfrcl2  49829  eloppf  49833