Theorem nelne1 3052

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-ne 2956

This theorem is used by:  elnelne1  3072  difsnb  4768  fofinf1o  9321  fin23lem24  10400  fin23lem31  10421  ttukeylem7  10593  npomex  11081  drnglidl1ne0  20769  lbspss  21357  islbs3  21433  lbsextlem4  21439  ssdifidlprm  21642  obslbs  22036  hauspwpwf1  24306  ppiltx  27504  tglineneq  29113  lnopp2hpgb  29241  colopp  29247  plngrotlem1  29265  plngrotlem2  29266  lnssplnglem  29269  tgaaddcpbllem1  29349  tgaaddcpbl  29352  prlngmolem1  29430  prlngmolem2  29431  quadcgrprlng  29444  ex-pss  31029  drngidlhash  33983  mxidlmaxv  33993  mxidlprm  33995  drng0mxidl  34000  qsdrnglem2  34020  dflringlem3  34028  dflring3  34029  dflring4  34030  rsprprmprmidl  34054  1arithufdlem4  34079  ply1annnr  34335  irngnminplynz  34344  algextdeglem4  34352  unelldsys  34791  cntnevol  34861  fin2solem  38530  lshpnelb  40042  osumcllem10N  41023  pexmidlem7N  41034  dochsnkrlem1  42527  ricdrng1  43593  rpnnen3lem  44038  lvecpsslmod  49619