<gh_stars>0
{
  "citations" : [ {
    "textCitation" : "[See disjss2 on Metamath](http://us.metamath.org/mpegif/disjss2.html)"
  } ],
  "names" : [ "disjss2" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_wral--1", "#T_vx", "#T_wral--2", "#T_cA", "#T_cB", "#T_wss", "#T_cC", "#T_wi", "#T_wdisj--1", "#T_vx", "#T_wdisj--2", "#T_cA", "#T_cC", "#T_wi", "#T_wdisj--1", "#T_vx", "#T_wdisj--2", "#T_cA", "#T_cB" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " If each element of a collection is contained in a disjoint collection, the original collection is also disjoint.  (Contributed by <NAME>, 14-Nov-2016.) ",
  "statement" : "disjss2 $p |- ( A. x e. A B C_ C -> ( Disj_ x e. A C -> Disj_ x e. A B ) ) $."
}