Theorem nelsn 4669

Description: If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.)

Assertion

Ref	Expression
nelsn	⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})

Proof of Theorem nelsn

Step	Hyp	Ref	Expression
1		elsni 4646	. 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2	1	necon3ai 2962	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2099   ≠ wne 2937  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-sn 4630

This theorem is referenced by:  frd  5637  fvn0fvelrn  6928  fvunsn  7188  nnoddn2prmb  16782  lbsextlem4  21049  cnfldfun  21293  cnfldfunOLD  21306  obslbs  21664  logbgcd1irr  26739  upgrres1  29139  cycpmco2  32867  lindssn  33106  drngidlhash  33163  drnglidl1ne0  33201  drng0mxidl  33202  ig1pmindeg  33272  irngnminplynz  33382  algextdeglem4  33388  submateqlem1  33408  submateqlem2  33409  qqhval2  33583  derangsn  34780  ricdrng1  41764  prjspersym  42031  prjspreln0  42033  prjspvs  42034  prjspnvs  42044  pr2eldif1  42984  pr2eldif2  42985  clsk3nimkb  43470  clsk1indlem1  43475  disjf1o  44564  cnrefiisplem  45217  fperdvper  45307  dvnmul  45331  wallispi  45458  etransc  45671  gsumge0cl  45759  meadjiunlem  45853  hspmbllem2  46015

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »