Theorem nelne1 3061

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-ne 2965

This theorem is referenced by:  elnelne1  3081  difsnb  4776  fofinf1o  9289  fin23lem24  10306  fin23lem31  10327  ttukeylem7  10499  npomex  10981  drnglidl1ne0  20602  lbspss  21181  islbs3  21257  lbsextlem4  21263  ssdifidlprm  21455  obslbs  21849  hauspwpwf1  24113  ppiltx  27307  tglineneq  28880  lnopp2hpgb  29004  colopp  29010  plngrotlem1  29027  plngrotlem2  29028  lnssplnglem  29031  prlngmolem1  29155  prlngmolem2  29156  ex-pss  30720  drngidlhash  33686  mxidlmaxv  33696  mxidlprm  33698  drng0mxidl  33703  qsdrnglem2  33723  dflringlem3  33731  dflring3  33732  dflring4  33733  rsprprmprmidl  33757  1arithufdlem4  33782  ply1annnr  34038  irngnminplynz  34047  algextdeglem4  34055  unelldsys  34493  cntnevol  34563  fin2solem  38180  lshpnelb  39683  osumcllem10N  40664  pexmidlem7N  40675  dochsnkrlem1  42168  ricdrng1  43223  rpnnen3lem  43685  lvecpsslmod  49207