Metamath Proof Explorer

Theorem brcosscnv2

Description: A and B are cosets by converse R : a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019)

Ref Expression
Assertion brcosscnv2 ⊢ A ∈ V ∧ B ∈ W → A ≀ R -1 B ↔ A R ∩ B R ≠ ∅

Proof

Step Hyp Ref Expression
1 brcosscnv ⊢ A ∈ V ∧ B ∈ W → A ≀ R -1 B ↔ ∃ x A R x ∧ B R x
2 ecinn0 ⊢ A ∈ V ∧ B ∈ W → A R ∩ B R ≠ ∅ ↔ ∃ x A R x ∧ B R x
3 1 2 bitr4d ⊢ A ∈ V ∧ B ∈ W → A ≀ R -1 B ↔ A R ∩ B R ≠ ∅