{
  "citations" : [ {
    "textCitation" : "[See eldifvsn on Metamath](http://us.metamath.org/mpegif/eldifvsn.html)"
  } ],
  "names" : [ "eldifvsn" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_cA", "#T_wcel", "#T_cV", "#T_wi", "#T_cA", "#T_wcel", "#T_cvv", "#T_cdif", "#T_csn--1", "#T_cB", "#T_csn--2", "#T_wb", "#T_cA", "#T_wne", "#T_cB" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " A set is an element of the universal class excluding a singleton iff it is not the singleton element.  (Contributed by AV, 7-Apr-2019.) ",
  "statement" : "eldifvsn $p |- ( A e. V -> ( A e. ( _V \\ { B } ) <-> A =/= B ) ) $."
}