Theorem nelne2 3054

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-ne 2957

This theorem is used by:  nelelne  3057  elnelne2  3074  elneeldif  3913  elpwdifsn  4752  f1ounsn  7280  ac5num  10115  infpssrlem4  10384  fpwwe2lem12  10727  zgt1rpn0n1  13163  cats1un  14870  dprdfadd  20236  dprdcntz2  20254  lbsextlem4  21439  lindff1  22126  hauscmplem  23724  fileln0  24169  zcld  25133  dvcnvlem  26296  ppinprm  27479  chtnprm  27481  tglnpt4  29123  footexALT  29193  footexlem1  29194  footexlem2  29195  foot  29197  colperpexlem3  29208  mideulem2  29210  opphllem  29211  opphllem2  29224  lnopp2hpgb  29241  colhp  29248  plngrotlem1  29265  plngrotlem2  29266  plngrot  29268  lnssplnglem  29269  lmieu  29289  trgcopy  29311  trgcopyeulem  29312  ragraghl  29346  tgaaddcpbllem1  29349  tgaaddcpbl  29352  perpprlng  29428  prlngex  29429  prlngmolem1  29430  prlngmid2  29439  quadcgrprlng  29444  cycpmco2lem1  33687  cycpmco2  33694  cyc3genpmlem  33712  unitnz  33799  fracfld  33870  linds2eq  33936  elrspunsn  33979  mxidlnzr  33992  lindsunlem  34256  fedgmul  34263  extdg1id  34298  2sqr3minply  34412  cos9thpiminplylem2  34415  ordtconnlem1  34556  esum2dlem  34724  subfacp1lem5  35949  heiborlem6  38750  llnle  40575  lplnle  40597  lhpexle1lem  41064  cdleme18b  41349  cdlemg46  41792  cdlemh  41874  ine1  43371  bcc0  45323  fnchoice  46045  climxrre  46759  stoweidlem43  47052  zneoALTV  48766  oppfrcllem  50234  oppfrcl2  50236  eloppf  50240