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

Metamath Proof Explorer

Theorem eldisjn0elb

Description: Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024)

Ref Expression
Assertion eldisjn0elb ⊢ ElDisj A ∧ ¬ ∅ ∈ A ↔ Disj E -1 ↾ A ∧ dom ⁡ E -1 ↾ A / E -1 ↾ A = A

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
2 n0el3 ⊢ ¬ ∅ ∈ A ↔ dom ⁡ E -1 ↾ A / E -1 ↾ A = A
3 1 2 anbi12i ⊢ ElDisj A ∧ ¬ ∅ ∈ A ↔ Disj E -1 ↾ A ∧ dom ⁡ E -1 ↾ A / E -1 ↾ A = A