Theorem nelne1 3054

Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)

Assertion

Ref	Expression
nelne1	⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Proof of Theorem nelne1

Step	Hyp	Ref	Expression
1		nelneq2 2887	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶)
2	1	neqned 2964	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-ne 2958

This theorem is used by:  elnelne1  3074  difsnb  4772  fofinf1o  9302  fin23lem24  10327  fin23lem31  10348  ttukeylem7  10520  npomex  11008  drnglidl1ne0  20680  lbspss  21267  islbs3  21343  lbsextlem4  21349  ssdifidlprm  21550  obslbs  21944  hauspwpwf1  24214  ppiltx  27411  tglineneq  28990  lnopp2hpgb  29118  colopp  29124  plngrotlem1  29142  plngrotlem2  29143  lnssplnglem  29146  tgaaddcpbllem1  29226  tgaaddcpbl  29229  prlngmolem1  29295  prlngmolem2  29296  quadcgrprlng  29309  ex-pss  30894  drngidlhash  33848  mxidlmaxv  33858  mxidlprm  33860  drng0mxidl  33865  qsdrnglem2  33885  dflringlem3  33893  dflring3  33894  dflring4  33895  rsprprmprmidl  33919  1arithufdlem4  33944  ply1annnr  34200  irngnminplynz  34209  algextdeglem4  34217  unelldsys  34656  cntnevol  34726  fin2solem  38347  lshpnelb  39844  osumcllem10N  40825  pexmidlem7N  40836  dochsnkrlem1  42329  ricdrng1  43397  rpnnen3lem  43859  lvecpsslmod  49424