Theorem ress0

Description: All restrictions of the empty set are trivial. (Contributed by Stefan O'Rear, 29-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	ress0	⊢ ( ∅ ↾s 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐴
2		0ex	⊢ ∅ ∈ V
3		eqid	⊢ ( ∅ ↾s 𝐴 ) = ( ∅ ↾s 𝐴 )
4		base0	⊢ ∅ = ( Base ‘ ∅ )
5	3 4	ressid2	⊢ ( ( ∅ ⊆ 𝐴 ∧ ∅ ∈ V ∧ 𝐴 ∈ V ) → ( ∅ ↾s 𝐴 ) = ∅ )
6	1 2 5	mp3an12	⊢ ( 𝐴 ∈ V → ( ∅ ↾s 𝐴 ) = ∅ )
7		reldmress	⊢ Rel dom ↾s
8	7	ovprc2	⊢ ( ¬ 𝐴 ∈ V → ( ∅ ↾s 𝐴 ) = ∅ )
9	6 8	pm2.61i	⊢ ( ∅ ↾s 𝐴 ) = ∅