No, it isn’t. The only primitive relations in ZFC are set membership and possibly equality (depending on how you prefer it). “x is a subset of y” is defined to mean “for all z, z in x implies z in y”.
Can I downvote myself? Somehow my mind switched “subset” and “membership”, and by the virtue of ZFC being a one-sorted theory, lo and behold, I wrote the above absurdity. Anyway, to rewrite the sentence and make it less wrong: subsets(x,y) is defined by the means of a first-order formula through the membership relation, which in a one-sorted theory already pertains the idea of ‘subsetting’. x E y --> {x} ⇐ y. So subsetting can be seen as a transfinite extension of the membership relation, and in ZFC we get no more clarity or computational intuition from the first than from the second.
No, it isn’t. The only primitive relations in ZFC are set membership and possibly equality (depending on how you prefer it). “x is a subset of y” is defined to mean “for all z, z in x implies z in y”.
Can I downvote myself? Somehow my mind switched “subset” and “membership”, and by the virtue of ZFC being a one-sorted theory, lo and behold, I wrote the above absurdity. Anyway, to rewrite the sentence and make it less wrong: subsets(x,y) is defined by the means of a first-order formula through the membership relation, which in a one-sorted theory already pertains the idea of ‘subsetting’. x E y --> {x} ⇐ y. So subsetting can be seen as a transfinite extension of the membership relation, and in ZFC we get no more clarity or computational intuition from the first than from the second.