Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dfeldisj2 | |- ( ElDisj A <-> ,~ `' ( `' _E |` A ) C_ _I ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-eldisj | |- ( ElDisj A <-> Disj ( `' _E |` A ) ) |
|
2 | relres | |- Rel ( `' _E |` A ) |
|
3 | dfdisjALTV2 | |- ( Disj ( `' _E |` A ) <-> ( ,~ `' ( `' _E |` A ) C_ _I /\ Rel ( `' _E |` A ) ) ) |
|
4 | 2 3 | mpbiran2 | |- ( Disj ( `' _E |` A ) <-> ,~ `' ( `' _E |` A ) C_ _I ) |
5 | 1 4 | bitri | |- ( ElDisj A <-> ,~ `' ( `' _E |` A ) C_ _I ) |