Metamath Proof Explorer


Theorem brcoss3

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

Ref Expression
Assertion brcoss3 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵 ↔ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 brcnvg ( ( 𝐴𝑉𝑢 ∈ V ) → ( 𝐴 𝑅 𝑢𝑢 𝑅 𝐴 ) )
2 1 elvd ( 𝐴𝑉 → ( 𝐴 𝑅 𝑢𝑢 𝑅 𝐴 ) )
3 brcnvg ( ( 𝐵𝑊𝑢 ∈ V ) → ( 𝐵 𝑅 𝑢𝑢 𝑅 𝐵 ) )
4 3 elvd ( 𝐵𝑊 → ( 𝐵 𝑅 𝑢𝑢 𝑅 𝐵 ) )
5 2 4 bi2anan9 ( ( 𝐴𝑉𝐵𝑊 ) → ( ( 𝐴 𝑅 𝑢𝐵 𝑅 𝑢 ) ↔ ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )
6 5 exbidv ( ( 𝐴𝑉𝐵𝑊 ) → ( ∃ 𝑢 ( 𝐴 𝑅 𝑢𝐵 𝑅 𝑢 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )
7 ecinn0 ( ( 𝐴𝑉𝐵𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ∃ 𝑢 ( 𝐴 𝑅 𝑢𝐵 𝑅 𝑢 ) ) )
8 brcoss ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )
9 6 7 8 3bitr4rd ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵 ↔ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ) )