Description: Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eleldisjs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseq2 | |
|
2 | 1 | eleq1d | |
3 | df-eldisjs | |
|
4 | 2 3 | elab2g | |