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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ 𝑅 𝐵 ↔ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 brcosscnv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ 𝑅 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
2 ecinn0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
3 1 2 bitr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ◡ 𝑅 𝐵 ↔ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ) )