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 ( ( 𝐵𝑉𝐶𝑊 ) → ( 𝐵𝐴 𝐶 ↔ ∃ 𝑢𝐴 ( 𝐵𝑢𝐶𝑢 ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ( 𝑥 = 𝐵 → ( 𝑥𝑢𝐵𝑢 ) )
2 eleq1 ( 𝑦 = 𝐶 → ( 𝑦𝑢𝐶𝑢 ) )
3 1 2 bi2anan9 ( ( 𝑥 = 𝐵𝑦 = 𝐶 ) → ( ( 𝑥𝑢𝑦𝑢 ) ↔ ( 𝐵𝑢𝐶𝑢 ) ) )
4 3 rexbidv ( ( 𝑥 = 𝐵𝑦 = 𝐶 ) → ( ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) ↔ ∃ 𝑢𝐴 ( 𝐵𝑢𝐶𝑢 ) ) )
5 dfcoels 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) }
6 4 5 brabga ( ( 𝐵𝑉𝐶𝑊 ) → ( 𝐵𝐴 𝐶 ↔ ∃ 𝑢𝐴 ( 𝐵𝑢𝐶𝑢 ) ) )