Line 555669

[Mázsa Péter]

After my PR https://github.com/metamath/set.mm/pull/4531/files ,
someone added the 555669 line to set.mm:
555668 Peter Mazsa, 16-Jun-2024.)
555669 [dferALTV2 on { A } + pet imply ( dom |` { A } ) /. |` { A } )
) = { A } ]
555670 $)
555671 trressn $p |-

i.e. that
dferALTV2 $p |- ( ,~ ( R |X. ( `' _E |` { A } ) ) ErALTV { A } <-> (
EqvRel ,~ ( R |X. ( `' _E |` { A } ) ) /\ ( dom ,~ ( R |X. ( `' _E |`
{ A } ) ) /. ,~ ( R |X. ( `' _E |` { A } ) ) ) = { A } ) ) and
pet $p |- ( ( R |X. ( `' _E |` { A } ) ) Part { A } <-> ,~ ( R |X. (
`' _E |` { A } ) ) ErALTV { A } )
(and perhaps
eqvrel1cossressn $p |- ( A e. V -> EqvRel ,~ ( R |X. ( `' _E |` { A } ) ) ) and
disjressn $p |- Disj ( R |X. ( `' _E |` { A } ) ) )
would somehow imply
( dom ( R |X. ( `' _E |` { A } ) ) /. ( R |X. ( `' _E |` { A } ) ) ) = { A } .

I would be happy if this were true: does the person who added 555669
remember the train of thought?

P.