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 400   ∈ wcel 2142   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

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

This theorem is used by:  elnelne1  3074  difsnb  4773  fofinf1o  9287  fin23lem24  10312  fin23lem31  10333  ttukeylem7  10505  npomex  10987  drnglidl1ne0  20627  lbspss  21214  islbs3  21290  lbsextlem4  21296  ssdifidlprm  21497  obslbs  21891  hauspwpwf1  24155  ppiltx  27352  tglineneq  28929  lnopp2hpgb  29056  colopp  29062  plngrotlem1  29080  plngrotlem2  29081  lnssplnglem  29084  prlngmolem1  29213  prlngmolem2  29214  quadcgrprlng  29227  ex-pss  30790  drngidlhash  33750  mxidlmaxv  33760  mxidlprm  33762  drng0mxidl  33767  qsdrnglem2  33787  dflringlem3  33795  dflring3  33796  dflring4  33797  rsprprmprmidl  33821  1arithufdlem4  33846  ply1annnr  34102  irngnminplynz  34111  algextdeglem4  34119  unelldsys  34557  cntnevol  34627  fin2solem  38285  lshpnelb  39786  osumcllem10N  40767  pexmidlem7N  40778  dochsnkrlem1  42271  ricdrng1  43324  rpnnen3lem  43786  lvecpsslmod  49315