Theorem nelne2 3040

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-ne 2941

This theorem is referenced by:  nelelne  3041  elnelne2  3058  elneeldif  3965  elpwdifsn  4789  f1ounsn  7292  ac5num  10076  infpssrlem4  10346  fpwwe2lem12  10682  zgt1rpn0n1  13076  cats1un  14759  dprdfadd  20040  dprdcntz2  20058  lbsextlem4  21163  lindff1  21840  hauscmplem  23414  fileln0  23858  zcld  24835  dvcnvlem  26014  ppinprm  27195  chtnprm  27197  footexALT  28726  footexlem1  28727  footexlem2  28728  foot  28730  colperpexlem3  28740  mideulem2  28742  opphllem  28743  opphllem2  28756  lnopp2hpgb  28771  colhp  28778  lmieu  28792  trgcopy  28812  trgcopyeulem  28813  cycpmco2lem1  33146  cycpmco2  33153  cyc3genpmlem  33171  unitnz  33243  fracfld  33310  linds2eq  33409  elrspunsn  33457  mxidlnzr  33495  lindsunlem  33675  fedgmul  33682  extdg1id  33716  2sqr3minply  33791  ordtconnlem1  33923  esum2dlem  34093  subfacp1lem5  35189  heiborlem6  37823  llnle  39520  lplnle  39542  lhpexle1lem  40009  cdleme18b  40294  cdlemg46  40737  cdlemh  40819  ine1  42349  bcc0  44359  fnchoice  45034  climxrre  45765  stoweidlem43  46058  zneoALTV  47656