Theorem nelne2 3030

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-ne 2933

This theorem is referenced by:  nelelne  3031  elnelne2  3048  elneeldif  3903  elpwdifsn  4734  f1ounsn  7227  ac5num  9958  infpssrlem4  10228  fpwwe2lem12  10565  zgt1rpn0n1  12985  cats1un  14683  dprdfadd  19997  dprdcntz2  20015  lbsextlem4  21159  lindff1  21800  hauscmplem  23371  fileln0  23815  zcld  24779  dvcnvlem  25943  ppinprm  27115  chtnprm  27117  footexALT  28786  footexlem1  28787  footexlem2  28788  foot  28790  colperpexlem3  28800  mideulem2  28802  opphllem  28803  opphllem2  28816  lnopp2hpgb  28831  colhp  28838  lmieu  28852  trgcopy  28872  trgcopyeulem  28873  cycpmco2lem1  33187  cycpmco2  33194  cyc3genpmlem  33212  unitnz  33300  fracfld  33369  linds2eq  33441  elrspunsn  33489  mxidlnzr  33527  lindsunlem  33768  fedgmul  33775  extdg1id  33810  2sqr3minply  33924  cos9thpiminplylem2  33927  ordtconnlem1  34068  esum2dlem  34236  subfacp1lem5  35366  mh-inf3f1  36723  heiborlem6  38137  llnle  39964  lplnle  39986  lhpexle1lem  40453  cdleme18b  40738  cdlemg46  41181  cdlemh  41263  ine1  42746  bcc0  44767  fnchoice  45460  climxrre  46178  stoweidlem43  46471  zneoALTV  48145  oppfrcllem  49602  oppfrcl2  49604  eloppf  49608