Metamath Proof Explorer

Theorem fences3

Description: Implication of eqvrelqseqdisj2 and n0eldmqseq , see comment of fences . (Contributed by Peter Mazsa, 30-Dec-2024)

Ref Expression
Assertion fences3 ⊢ EqvRel R ∧ dom ⁡ R / R = A → ElDisj A ∧ ¬ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj2 ⊢ EqvRel R ∧ dom ⁡ R / R = A → ElDisj A
2 n0eldmqseq ⊢ dom ⁡ R / R = A → ¬ ∅ ∈ A
3 2 adantl ⊢ EqvRel R ∧ dom ⁡ R / R = A → ¬ ∅ ∈ A
4 1 3 jca ⊢ EqvRel R ∧ dom ⁡ R / R = A → ElDisj A ∧ ¬ ∅ ∈ A