fof(union_comm,conjecture,union(fA,fB)=union(fB,fA)).
fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))).
fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)).
------------------
fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))).
fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)).
fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))).
fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)).
------------------
fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC)))).
fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)).
fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))).
fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)).
fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))).
------------------
fof(union_assoc,conjecture,union(union(fA,fB),fC)=union(fA,union(fB,fC))).
fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)).
fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))).
fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)).
fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC)))).
fof(union_assoc2,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))).