Step |
Hyp |
Ref |
Expression |
1 |
|
df-wunc |
⊢ wUniCl = ( 𝑥 ∈ V ↦ ∩ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 } ) |
2 |
|
sseq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑢 ↔ 𝐴 ⊆ 𝑢 ) ) |
3 |
2
|
rabbidv |
⊢ ( 𝑥 = 𝐴 → { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 } = { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ) |
4 |
3
|
inteqd |
⊢ ( 𝑥 = 𝐴 → ∩ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 } = ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ) |
5 |
|
elex |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) |
6 |
|
wunex |
⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 ) |
7 |
|
rabn0 |
⊢ ( { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ≠ ∅ ↔ ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 ) |
8 |
6 7
|
sylibr |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ≠ ∅ ) |
9 |
|
intex |
⊢ ( { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ≠ ∅ ↔ ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ∈ V ) |
10 |
8 9
|
sylib |
⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ∈ V ) |
11 |
1 4 5 10
|
fvmptd3 |
⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) = ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ) |