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