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