Metamath Proof Explorer


Theorem brcoss

Description: A and B are cosets by R : a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018)

Ref Expression
Assertion brcoss ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑥 = 𝐴 → ( 𝑢 𝑅 𝑥𝑢 𝑅 𝐴 ) )
2 breq2 ( 𝑦 = 𝐵 → ( 𝑢 𝑅 𝑦𝑢 𝑅 𝐵 ) )
3 1 2 bi2anan9 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( 𝑢 𝑅 𝑥𝑢 𝑅 𝑦 ) ↔ ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )
4 3 exbidv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ∃ 𝑢 ( 𝑢 𝑅 𝑥𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )
5 df-coss 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥𝑢 𝑅 𝑦 ) }
6 4 5 brabga ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )