Metamath Proof Explorer


Theorem eleldisjs

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

Ref Expression
Assertion eleldisjs AVAElDisjsE-1ADisjs

Proof

Step Hyp Ref Expression
1 reseq2 a=AE-1a=E-1A
2 1 eleq1d a=AE-1aDisjsE-1ADisjs
3 df-eldisjs ElDisjs=a|E-1aDisjs
4 2 3 elab2g AVAElDisjsE-1ADisjs