Description: The domain quotient predicate for the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvepresdmqs | |- ( ( `' _E |` A ) DomainQs A <-> -. (/) e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-dmqs | |- ( ( `' _E |` A ) DomainQs A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) |
|
| 2 | n0el3 | |- ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) |
|
| 3 | 1 2 | bitr4i | |- ( ( `' _E |` A ) DomainQs A <-> -. (/) e. A ) |