Description: Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eleldisjs | |- ( A e. V -> ( A e. ElDisjs <-> ( `' _E |` A ) e. Disjs ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reseq2 | |- ( a = A -> ( `' _E |` a ) = ( `' _E |` A ) ) |
|
2 | 1 | eleq1d | |- ( a = A -> ( ( `' _E |` a ) e. Disjs <-> ( `' _E |` A ) e. Disjs ) ) |
3 | df-eldisjs | |- ElDisjs = { a | ( `' _E |` a ) e. Disjs } |
|
4 | 2 3 | elab2g | |- ( A e. V -> ( A e. ElDisjs <-> ( `' _E |` A ) e. Disjs ) ) |