Step |
Hyp |
Ref |
Expression |
1 |
|
in0 |
⊢ ( 𝐴 ∩ ∅ ) = ∅ |
2 |
|
incom |
⊢ ( 𝐴 ∩ ∅ ) = ( ∅ ∩ 𝐴 ) |
3 |
1 2
|
eqtr3i |
⊢ ∅ = ( ∅ ∩ 𝐴 ) |
4 |
|
0ex |
⊢ ∅ ∈ V |
5 |
|
eleq1 |
⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝑋 ↔ ∅ ∈ 𝑋 ) ) |
6 |
|
ineq1 |
⊢ ( 𝑥 = ∅ → ( 𝑥 ∩ 𝐴 ) = ( ∅ ∩ 𝐴 ) ) |
7 |
6
|
eqeq2d |
⊢ ( 𝑥 = ∅ → ( ∅ = ( 𝑥 ∩ 𝐴 ) ↔ ∅ = ( ∅ ∩ 𝐴 ) ) ) |
8 |
5 7
|
anbi12d |
⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝑋 ∧ ∅ = ( 𝑥 ∩ 𝐴 ) ) ↔ ( ∅ ∈ 𝑋 ∧ ∅ = ( ∅ ∩ 𝐴 ) ) ) ) |
9 |
4 8
|
spcev |
⊢ ( ( ∅ ∈ 𝑋 ∧ ∅ = ( ∅ ∩ 𝐴 ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ ∅ = ( 𝑥 ∩ 𝐴 ) ) ) |
10 |
3 9
|
mpan2 |
⊢ ( ∅ ∈ 𝑋 → ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ ∅ = ( 𝑥 ∩ 𝐴 ) ) ) |
11 |
|
df-rex |
⊢ ( ∃ 𝑥 ∈ 𝑋 ∅ = ( 𝑥 ∩ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ ∅ = ( 𝑥 ∩ 𝐴 ) ) ) |
12 |
10 11
|
sylibr |
⊢ ( ∅ ∈ 𝑋 → ∃ 𝑥 ∈ 𝑋 ∅ = ( 𝑥 ∩ 𝐴 ) ) |
13 |
|
elrest |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∅ ∈ ( 𝑋 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑋 ∅ = ( 𝑥 ∩ 𝐴 ) ) ) |
14 |
12 13
|
syl5ibr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∅ ∈ 𝑋 → ∅ ∈ ( 𝑋 ↾t 𝐴 ) ) ) |