Metamath Proof Explorer

Theorem eldisjs3

Description: Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion eldisjs3 ⊢ R ∈ Disjs ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v ∧ R ∈ Rels

Proof

Step Hyp Ref Expression
1 eldisjs2 ⊢ R ∈ Disjs ↔ ≀ R -1 ⊆ I ∧ R ∈ Rels
2 cosscnvssid3 ⊢ ≀ R -1 ⊆ I ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v
3 2 anbi1i ⊢ ≀ R -1 ⊆ I ∧ R ∈ Rels ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v ∧ R ∈ Rels
4 1 3 bitri ⊢ R ∈ Disjs ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v ∧ R ∈ Rels