Theorem brcoss2

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

	Ref	Expression
Assertion	brcoss2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝐴 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 ∈ [ 𝑢 ] 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brcoss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) )
2		exan3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑢 ( 𝐴 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 ∈ [ 𝑢 ] 𝑅 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) )
3	1 2	bitr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝐴 ∈ [ 𝑢 ] 𝑅 ∧ 𝐵 ∈ [ 𝑢 ] 𝑅 ) ) )