Metamath Proof Explorer

Theorem br1cossinidres

Description: B and C are cosets by an intersection with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion br1cossinidres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ I ↾ A C ↔ ∃ u ∈ A u = B ∧ u R B ∧ u = C ∧ u R C

Proof

Step Hyp Ref Expression
1 br1cossinres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ I ↾ A C ↔ ∃ u ∈ A u I B ∧ u R B ∧ u I C ∧ u R C
2 ideq2 ⊢ u ∈ V → u I B ↔ u = B
3 2 elv ⊢ u I B ↔ u = B
4 3 anbi1i ⊢ u I B ∧ u R B ↔ u = B ∧ u R B
5 ideq2 ⊢ u ∈ V → u I C ↔ u = C
6 5 elv ⊢ u I C ↔ u = C
7 6 anbi1i ⊢ u I C ∧ u R C ↔ u = C ∧ u R C
8 4 7 anbi12i ⊢ u I B ∧ u R B ∧ u I C ∧ u R C ↔ u = B ∧ u R B ∧ u = C ∧ u R C
9 8 rexbii ⊢ ∃ u ∈ A u I B ∧ u R B ∧ u I C ∧ u R C ↔ ∃ u ∈ A u = B ∧ u R B ∧ u = C ∧ u R C
10 1 9 bitrdi ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ I ↾ A C ↔ ∃ u ∈ A u = B ∧ u R B ∧ u = C ∧ u R C