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	⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		cnvepresex	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V )
2		brdmqss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ◡ E ↾ 𝐴 ) ∈ V ) → ( ( ◡ E ↾ 𝐴 ) DomainQss 𝐴 ↔ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )
3	1 2	mpdan	⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) DomainQss 𝐴 ↔ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )
4		n0el3	⊢ ( ¬ ∅ ∈ 𝐴 ↔ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 )
5	3 4	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴 ) )