Step |
Hyp |
Ref |
Expression |
1 |
|
compss.a |
⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) |
2 |
|
difeq2 |
⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑎 ) ) |
3 |
2
|
cbvmptv |
⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) = ( 𝑎 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑎 ) ) |
4 |
1 3
|
eqtri |
⊢ 𝐹 = ( 𝑎 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑎 ) ) |
5 |
|
difeq2 |
⊢ ( 𝑎 = 𝑋 → ( 𝐴 ∖ 𝑎 ) = ( 𝐴 ∖ 𝑋 ) ) |
6 |
|
elpw2g |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴 ) ) |
7 |
6
|
biimpar |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ∈ 𝒫 𝐴 ) |
8 |
|
difexg |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ 𝑋 ) ∈ V ) |
9 |
8
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐴 ∖ 𝑋 ) ∈ V ) |
10 |
4 5 7 9
|
fvmptd3 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐴 ∖ 𝑋 ) ) |