Metamath Proof Explorer


Theorem eldisjs3

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

Ref Expression
Assertion eldisjs3 ( 𝑅 ∈ Disjs ↔ ( ∀ 𝑢𝑣𝑥 ( ( 𝑢 𝑅 𝑥𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 eldisjs2 ( 𝑅 ∈ Disjs ↔ ( ≀ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) )
2 cosscnvssid3 ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢𝑣𝑥 ( ( 𝑢 𝑅 𝑥𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) )
3 2 anbi1i ( ( ≀ 𝑅 ⊆ I ∧ 𝑅 ∈ Rels ) ↔ ( ∀ 𝑢𝑣𝑥 ( ( 𝑢 𝑅 𝑥𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) ∧ 𝑅 ∈ Rels ) )
4 1 3 bitri ( 𝑅 ∈ Disjs ↔ ( ∀ 𝑢𝑣𝑥 ( ( 𝑢 𝑅 𝑥𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) ∧ 𝑅 ∈ Rels ) )