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 2145   ≠ wne 2955

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 2732

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

This theorem is used by:  elnelne1  3072  difsnb  4769  fofinf1o  9299  fin23lem24  10357  fin23lem31  10378  ttukeylem7  10550  npomex  11038  drnglidl1ne0  20716  lbspss  21304  islbs3  21380  lbsextlem4  21386  ssdifidlprm  21589  obslbs  21983  hauspwpwf1  24253  ppiltx  27453  tglineneq  29032  lnopp2hpgb  29160  colopp  29166  plngrotlem1  29184  plngrotlem2  29185  lnssplnglem  29188  tgaaddcpbllem1  29268  tgaaddcpbl  29271  prlngmolem1  29349  prlngmolem2  29350  quadcgrprlng  29363  ex-pss  30948  drngidlhash  33902  mxidlmaxv  33912  mxidlprm  33914  drng0mxidl  33919  qsdrnglem2  33939  dflringlem3  33947  dflring3  33948  dflring4  33949  rsprprmprmidl  33973  1arithufdlem4  33998  ply1annnr  34254  irngnminplynz  34263  algextdeglem4  34271  unelldsys  34710  cntnevol  34780  fin2solem  38443  lshpnelb  39955  osumcllem10N  40936  pexmidlem7N  40947  dochsnkrlem1  42440  ricdrng1  43508  rpnnen3lem  43970  lvecpsslmod  49535