Metamath Proof Explorer

Theorem br1cossxrnidres

Description: <. B , C >. and <. D , E >. are cosets by a range Cartesian product with the restricted identity class: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021)

Ref Expression
Assertion br1cossxrnidres ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → B C ≀ R ⋉ I ↾ A D E ↔ ∃ u ∈ A u = C ∧ u R B ∧ u = E ∧ u R D

Proof

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