Metamath Proof Explorer
Description: All restrictions of the null 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 𝐴 ) = ∅ |