Description: Alternate proof of pw0 . The proofs have a similar structure: pw0 uses the definitions of powerclass and singleton as class abstractions,
whereas bj-pw0ALT uses characterizations of their elements. Both proofs
then use transitivity of a congruence relation (equality for pw0 and
biconditional for bj-pw0ALT ) to translate the property ss0b into the
wanted result. To translate a biconditional into a class equality, pw0 uses abbii (which yields an equality of class abstractions), while
bj-pw0ALT uses eqriv (which requires a biconditional of membership of
a given setvar variable). Note that abbii , through its closed form
abbi1 , is proved from eqrdv , which is the deduction form of
eqriv . In the other direction, velpw and velsn are proved from the
definitions of powerclass and singleton using elabg , which is a version
of abbii suited for membership characterizations. (Contributed by BJ, 14-Apr-2024)(Proof modification is discouraged.)(New usage is discouraged.)