Metamath Proof Explorer

Theorem brcoels

Description: B and C are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020) (Revised by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion brcoels ⊢ B ∈ V ∧ C ∈ W → B ∼ A C ↔ ∃ u ∈ A B ∈ u ∧ C ∈ u

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ x = B → x ∈ u ↔ B ∈ u
2 eleq1 ⊢ y = C → y ∈ u ↔ C ∈ u
3 1 2 bi2anan9 ⊢ x = B ∧ y = C → x ∈ u ∧ y ∈ u ↔ B ∈ u ∧ C ∈ u
4 3 rexbidv ⊢ x = B ∧ y = C → ∃ u ∈ A x ∈ u ∧ y ∈ u ↔ ∃ u ∈ A B ∈ u ∧ C ∈ u
5 dfcoels ⊢ ∼ A = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
6 4 5 brabga ⊢ B ∈ V ∧ C ∈ W → B ∼ A C ↔ ∃ u ∈ A B ∈ u ∧ C ∈ u