Metamath Proof Explorer

Theorem dfdisjALTV3

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV3 . (Contributed by Peter Mazsa, 28-Jul-2021)

Ref Expression
Assertion dfdisjALTV3 ⊢ Disj R ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dfdisjALTV2 ⊢ Disj R ↔ ≀ R -1 ⊆ I ∧ Rel ⁡ R
2 cosscnvssid3 ⊢ ≀ R -1 ⊆ I ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v
3 2 anbi1i ⊢ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v ∧ Rel ⁡ R
4 1 3 bitri ⊢ Disj R ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v ∧ Rel ⁡ R