Metamath Proof Explorer


Theorem eleldisjs

Description: Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023)

Ref Expression
Assertion eleldisjs A V A ElDisjs E -1 A Disjs

Proof

Step Hyp Ref Expression
1 reseq2 a = A E -1 a = E -1 A
2 1 eleq1d a = A E -1 a Disjs E -1 A Disjs
3 df-eldisjs ElDisjs = a | E -1 a Disjs
4 2 3 elab2g A V A ElDisjs E -1 A Disjs