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