Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1400.1 |
⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 ) |
2 |
|
dmuni |
⊢ dom ∪ 𝐴 = ∪ 𝑧 ∈ 𝐴 dom 𝑧 |
3 |
|
df-iun |
⊢ ∪ 𝑥 ∈ 𝐴 dom 𝑥 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 } |
4 |
|
df-iun |
⊢ ∪ 𝑧 ∈ 𝐴 dom 𝑧 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 } |
5 |
1
|
nfcii |
⊢ Ⅎ 𝑥 𝐴 |
6 |
|
nfcv |
⊢ Ⅎ 𝑧 𝐴 |
7 |
|
nfv |
⊢ Ⅎ 𝑧 𝑦 ∈ dom 𝑥 |
8 |
|
nfv |
⊢ Ⅎ 𝑥 𝑦 ∈ dom 𝑧 |
9 |
|
dmeq |
⊢ ( 𝑥 = 𝑧 → dom 𝑥 = dom 𝑧 ) |
10 |
9
|
eleq2d |
⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ dom 𝑥 ↔ 𝑦 ∈ dom 𝑧 ) ) |
11 |
5 6 7 8 10
|
cbvrexfw |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 ) |
12 |
11
|
abbii |
⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 } |
13 |
4 12
|
eqtr4i |
⊢ ∪ 𝑧 ∈ 𝐴 dom 𝑧 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 } |
14 |
3 13
|
eqtr4i |
⊢ ∪ 𝑥 ∈ 𝐴 dom 𝑥 = ∪ 𝑧 ∈ 𝐴 dom 𝑧 |
15 |
2 14
|
eqtr4i |
⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥 |