This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvepresdmqss

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 ∈ V → E -1 ↾ A DomainQss A ↔ ¬ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 cnvepresex ⊢ A ∈ V → E -1 ↾ A ∈ V
2 brdmqss ⊢ A ∈ V ∧ E -1 ↾ A ∈ V → E -1 ↾ A DomainQss A ↔ dom ⁡ E -1 ↾ A / E -1 ↾ A = A
3 1 2 mpdan ⊢ A ∈ V → E -1 ↾ A DomainQss A ↔ dom ⁡ E -1 ↾ A / E -1 ↾ A = A
4 n0el3 ⊢ ¬ ∅ ∈ A ↔ dom ⁡ E -1 ↾ A / E -1 ↾ A = A
5 3 4 bitr4di ⊢ A ∈ V → E -1 ↾ A DomainQss A ↔ ¬ ∅ ∈ A