Metamath Proof Explorer

Theorem br1cossres2

Description: B and C are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 3-Jan-2018)

Ref Expression
Assertion br1cossres2 ⊢ B ∈ V ∧ C ∈ W → B ≀ R ↾ A C ↔ ∃ x ∈ A B ∈ x R ∧ C ∈ x R

Proof

Step Hyp Ref Expression
1 br1cossres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ↾ A C ↔ ∃ x ∈ A x R B ∧ x R C
2 exanres3 ⊢ B ∈ V ∧ C ∈ W → ∃ x ∈ A B ∈ x R ∧ C ∈ x R ↔ ∃ x ∈ A x R B ∧ x R C
3 1 2 bitr4d ⊢ B ∈ V ∧ C ∈ W → B ≀ R ↾ A C ↔ ∃ x ∈ A B ∈ x R ∧ C ∈ x R