Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
|
suppval |
⊢ ( ( ∅ ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ∅ supp 𝑍 ) = { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } ) |
3 |
1 2
|
mpan |
⊢ ( 𝑍 ∈ 𝑊 → ( ∅ supp 𝑍 ) = { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } ) |
4 |
|
dm0 |
⊢ dom ∅ = ∅ |
5 |
|
rabeq |
⊢ ( dom ∅ = ∅ → { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } ) |
6 |
4 5
|
mp1i |
⊢ ( 𝑍 ∈ 𝑊 → { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } ) |
7 |
|
rab0 |
⊢ { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = ∅ |
8 |
7
|
a1i |
⊢ ( 𝑍 ∈ 𝑊 → { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = ∅ ) |
9 |
3 6 8
|
3eqtrd |
⊢ ( 𝑍 ∈ 𝑊 → ( ∅ supp 𝑍 ) = ∅ ) |