Metamath Proof Explorer

Theorem 1cossres

Description: The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019)

Ref Expression
Assertion 1cossres ⊢ ≀ R ↾ A = x y | ∃ u ∈ A u R x ∧ u R y

Proof

Step Hyp Ref Expression
1 df-coss ⊢ ≀ R ↾ A = x y | ∃ u u R ↾ A x ∧ u R ↾ A y
2 df-rex ⊢ ∃ u ∈ A u R x ∧ u R y ↔ ∃ u u ∈ A ∧ u R x ∧ u R y
3 anandi ⊢ u ∈ A ∧ u R x ∧ u R y ↔ u ∈ A ∧ u R x ∧ u ∈ A ∧ u R y
4 brres ⊢ x ∈ V → u R ↾ A x ↔ u ∈ A ∧ u R x
5 4 elv ⊢ u R ↾ A x ↔ u ∈ A ∧ u R x
6 brres ⊢ y ∈ V → u R ↾ A y ↔ u ∈ A ∧ u R y
7 6 elv ⊢ u R ↾ A y ↔ u ∈ A ∧ u R y
8 5 7 anbi12i ⊢ u R ↾ A x ∧ u R ↾ A y ↔ u ∈ A ∧ u R x ∧ u ∈ A ∧ u R y
9 3 8 bitr4i ⊢ u ∈ A ∧ u R x ∧ u R y ↔ u R ↾ A x ∧ u R ↾ A y
10 9 exbii ⊢ ∃ u u ∈ A ∧ u R x ∧ u R y ↔ ∃ u u R ↾ A x ∧ u R ↾ A y
11 2 10 bitri ⊢ ∃ u ∈ A u R x ∧ u R y ↔ ∃ u u R ↾ A x ∧ u R ↾ A y
12 11 opabbii ⊢ x y | ∃ u ∈ A u R x ∧ u R y = x y | ∃ u u R ↾ A x ∧ u R ↾ A y
13 1 12 eqtr4i ⊢ ≀ R ↾ A = x y | ∃ u ∈ A u R x ∧ u R y