Description: The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is ( A e. ElDisjs <-> ElDisj A ) when A is a set. (Contributed by Peter Mazsa, 23-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eleldisjseldisj |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleldisjs | ||
2 | cnvepresex | ||
3 | eldisjsdisj | ||
4 | 2 3 | syl | |
5 | 1 4 | bitrd | |
6 | df-eldisj | ||
7 | 5 6 | bitr4di |