Metamath Proof Explorer

Theorem rnxrnres

Description: Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021)

Ref Expression
Assertion rnxrnres ⊢ ran ⁡ R ⋉ S ↾ A = x y | ∃ u ∈ A u R x ∧ u S y

Proof

Step Hyp Ref Expression
1 rnxrn ⊢ ran ⁡ R ⋉ S ↾ A = x y | ∃ u u R x ∧ u S ↾ A y
2 brres ⊢ y ∈ V → u S ↾ A y ↔ u ∈ A ∧ u S y
3 2 elv ⊢ u S ↾ A y ↔ u ∈ A ∧ u S y
4 3 anbi2i ⊢ u R x ∧ u S ↾ A y ↔ u R x ∧ u ∈ A ∧ u S y
5 an12 ⊢ u ∈ A ∧ u R x ∧ u S y ↔ u R x ∧ u ∈ A ∧ u S y
6 4 5 bitr4i ⊢ u R x ∧ u S ↾ A y ↔ u ∈ A ∧ u R x ∧ u S y
7 6 exbii ⊢ ∃ u u R x ∧ u S ↾ A y ↔ ∃ u u ∈ A ∧ u R x ∧ u S y
8 df-rex ⊢ ∃ u ∈ A u R x ∧ u S y ↔ ∃ u u ∈ A ∧ u R x ∧ u S y
9 7 8 bitr4i ⊢ ∃ u u R x ∧ u S ↾ A y ↔ ∃ u ∈ A u R x ∧ u S y
10 9 opabbii ⊢ x y | ∃ u u R x ∧ u S ↾ A y = x y | ∃ u ∈ A u R x ∧ u S y
11 1 10 eqtri ⊢ ran ⁡ R ⋉ S ↾ A = x y | ∃ u ∈ A u R x ∧ u S y