Step |
Hyp |
Ref |
Expression |
1 |
|
df-membpart |
|- ( MembPart A <-> ( `' _E |` A ) Part A ) |
2 |
|
df-part |
|- ( ( `' _E |` A ) Part A <-> ( Disj ( `' _E |` A ) /\ ( `' _E |` A ) DomainQs A ) ) |
3 |
|
df-eldisj |
|- ( ElDisj A <-> Disj ( `' _E |` A ) ) |
4 |
3
|
bicomi |
|- ( Disj ( `' _E |` A ) <-> ElDisj A ) |
5 |
|
cnvepresdmqs |
|- ( ( `' _E |` A ) DomainQs A <-> -. (/) e. A ) |
6 |
4 5
|
anbi12i |
|- ( ( Disj ( `' _E |` A ) /\ ( `' _E |` A ) DomainQs A ) <-> ( ElDisj A /\ -. (/) e. A ) ) |
7 |
1 2 6
|
3bitri |
|- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) |