Description: A biconditional connecting the conditional operator for propositions and the conditional operator for classes. Note that there is no sethood hypothesis on X : it is implied by either side. (Contributed by BJ, 24-Sep-2019) Generalize statement from setvar x to class X . (Revised by BJ, 26-Dec-2023)