Theorem nelne2 3039

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2106   ≠ wne 2939

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-ne 2940

This theorem is referenced by:  nelelne  3040  elnelne2  3057  elneeldif  3927  elpwdifsn  4754  ac5num  9981  infpssrlem4  10251  fpwwe2lem12  10587  zgt1rpn0n1  12965  cats1un  14621  dprdfadd  19813  dprdcntz2  19831  lbsextlem4  20681  lindff1  21263  hauscmplem  22794  fileln0  23238  zcld  24213  dvcnvlem  25377  ppinprm  26538  chtnprm  26540  footexALT  27723  footexlem1  27724  footexlem2  27725  foot  27727  colperpexlem3  27737  mideulem2  27739  opphllem  27740  opphllem2  27753  lnopp2hpgb  27768  colhp  27775  lmieu  27789  trgcopy  27809  trgcopyeulem  27810  cycpmco2lem1  32045  cycpmco2  32052  cyc3genpmlem  32070  linds2eq  32241  mxidlnzr  32312  lindsunlem  32406  fedgmul  32413  extdg1id  32439  ordtconnlem1  32594  esum2dlem  32780  subfacp1lem5  33865  heiborlem6  36348  llnle  38054  lplnle  38076  lhpexle1lem  38543  cdleme18b  38828  cdlemg46  39271  cdlemh  39353  bcc0  42742  fnchoice  43356  climxrre  44111  stoweidlem43  44404  zneoALTV  45981