Description: The domain quotient binary relation of 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 | cnvepresdmqss | |- ( A e. V -> ( ( `' _E |` A ) DomainQss A <-> -. (/) e. A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvepresex | |- ( A e. V -> ( `' _E |` A ) e. _V ) |
|
| 2 | brdmqss | |- ( ( A e. V /\ ( `' _E |` A ) e. _V ) -> ( ( `' _E |` A ) DomainQss A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) ) |
|
| 3 | 1 2 | mpdan | |- ( A e. V -> ( ( `' _E |` A ) DomainQss A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) ) |
| 4 | n0el3 | |- ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) |
|
| 5 | 3 4 | bitr4di | |- ( A e. V -> ( ( `' _E |` A ) DomainQss A <-> -. (/) e. A ) ) |