Description: The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015)