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 ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ ∃ u u R A ∧ u R B

Proof

Step Hyp Ref Expression
1 breq2 ⊢ x = A → u R x ↔ u R A
2 breq2 ⊢ y = B → u R y ↔ u R B
3 1 2 bi2anan9 ⊢ x = A ∧ y = B → u R x ∧ u R y ↔ u R A ∧ u R B
4 3 exbidv ⊢ x = A ∧ y = B → ∃ u u R x ∧ u R y ↔ ∃ u u R A ∧ u R B
5 df-coss ⊢ ≀ R = x y | ∃ u u R x ∧ u R y
6 4 5 brabga ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ ∃ u u R A ∧ u R B