Theorem nelne1 3056

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-ne 2960

This theorem is used by:  elnelne1  3076  difsnb  4769  fofinf1o  9346  fin23lem24  10424  fin23lem31  10445  ttukeylem7  10617  npomex  11105  drnglidl1ne0  20796  lbspss  21384  islbs3  21460  lbsextlem4  21466  ssdifidlprm  21669  obslbs  22063  hauspwpwf1  24333  ppiltx  27531  tglineneq  29140  lnopp2hpgb  29268  colopp  29274  plngrotlem1  29292  plngrotlem2  29293  lnssplnglem  29296  tgaaddcpbllem1  29376  tgaaddcpbl  29379  prlngmolem1  29457  prlngmolem2  29458  quadcgrprlng  29471  ex-pss  31056  drngidlhash  34050  mxidlmaxv  34060  mxidlprm  34062  drng0mxidl  34067  qsdrnglem2  34087  dflringlem3  34095  dflring3  34096  dflring4  34097  rsprprmprmidl  34121  1arithufdlem4  34146  ply1annnr  34402  irngnminplynz  34411  algextdeglem4  34419  unelldsys  34858  cntnevol  34928  fin2solem  38720  lshpnelb  40232  osumcllem10N  41213  pexmidlem7N  41224  dochsnkrlem1  42717  ricdrng1  43783  rpnnen3lem  44229  lvecpsslmod  49822