Description: Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 , unless A is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 10-Sep-2013)