Step |
Hyp |
Ref |
Expression |
1 |
|
df-part |
Could not format ( R Part A <-> ( Disj R /\ R DomainQs A ) ) : No typesetting found for |- ( R Part A <-> ( Disj R /\ R DomainQs A ) ) with typecode |- |
2 |
|
df-dmqs |
|
3 |
2
|
anbi2i |
|
4 |
1 3
|
bitri |
Could not format ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) : No typesetting found for |- ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) with typecode |- |