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 ( 𝐴 ↾ { 𝐵 } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( 𝐴 ↾ { 𝐵 } )
2 relxp ⊢ Rel ( { 𝐵 } × ( 𝐴 “ { 𝐵 } ) )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 elimasn ⊢ ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
6 elsni ⊢ ( 𝑥 ∈ { 𝐵 } → 𝑥 = 𝐵 )
7 6 sneqd ⊢ ( 𝑥 ∈ { 𝐵 } → { 𝑥 } = { 𝐵 } )
8 7 imaeq2d ⊢ ( 𝑥 ∈ { 𝐵 } → ( 𝐴 “ { 𝑥 } ) = ( 𝐴 “ { 𝐵 } ) )
9 8 eleq2d ⊢ ( 𝑥 ∈ { 𝐵 } → ( 𝑦 ∈ ( 𝐴 “ { 𝑥 } ) ↔ 𝑦 ∈ ( 𝐴 “ { 𝐵 } ) ) )
10 5 9 bitr3id ⊢ ( 𝑥 ∈ { 𝐵 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ 𝑦 ∈ ( 𝐴 “ { 𝐵 } ) ) )
11 10 pm5.32i ⊢ ( ( 𝑥 ∈ { 𝐵 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ↔ ( 𝑥 ∈ { 𝐵 } ∧ 𝑦 ∈ ( 𝐴 “ { 𝐵 } ) ) )
12 4 opelresi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ↾ { 𝐵 } ) ↔ ( 𝑥 ∈ { 𝐵 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
13 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝐵 } × ( 𝐴 “ { 𝐵 } ) ) ↔ ( 𝑥 ∈ { 𝐵 } ∧ 𝑦 ∈ ( 𝐴 “ { 𝐵 } ) ) )
14 11 12 13 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ↾ { 𝐵 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝐵 } × ( 𝐴 “ { 𝐵 } ) ) )
15 1 2 14 eqrelriiv ⊢ ( 𝐴 ↾ { 𝐵 } ) = ( { 𝐵 } × ( 𝐴 “ { 𝐵 } ) )