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