This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressn

Description: Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ressn ⊢ A ↾ B = B × A B

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ A ↾ B
2 relxp ⊢ Rel ⁡ B × A B
3 vex ⊢ x ∈ V
4 vex ⊢ y ∈ V
5 3 4 elimasn ⊢ y ∈ A x ↔ x y ∈ A
6 elsni ⊢ x ∈ B → x = B
7 6 sneqd ⊢ x ∈ B → x = B
8 7 imaeq2d ⊢ x ∈ B → A x = A B
9 8 eleq2d ⊢ x ∈ B → y ∈ A x ↔ y ∈ A B
10 5 9 bitr3id ⊢ x ∈ B → x y ∈ A ↔ y ∈ A B
11 10 pm5.32i ⊢ x ∈ B ∧ x y ∈ A ↔ x ∈ B ∧ y ∈ A B
12 4 opelresi ⊢ x y ∈ A ↾ B ↔ x ∈ B ∧ x y ∈ A
13 opelxp ⊢ x y ∈ B × A B ↔ x ∈ B ∧ y ∈ A B
14 11 12 13 3bitr4i ⊢ x y ∈ A ↾ B ↔ x y ∈ B × A B
15 1 2 14 eqrelriiv ⊢ A ↾ B = B × A B