Step |
Hyp |
Ref |
Expression |
1 |
|
iuneq12d.1 |
⊢ ( 𝜑 → 𝐴 = 𝐵 ) |
2 |
|
iuneq12d.2 |
⊢ ( 𝜑 → 𝐶 = 𝐷 ) |
3 |
1
|
eleq2d |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) |
4 |
3
|
anbi1d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑡 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑡 ∈ 𝐶 ) ) ) |
5 |
4
|
rexbidv2 |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑡 ∈ 𝐶 ) ) |
6 |
5
|
abbidv |
⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 } = { 𝑡 ∣ ∃ 𝑥 ∈ 𝐵 𝑡 ∈ 𝐶 } ) |
7 |
|
df-iun |
⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = { 𝑡 ∣ ∃ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐶 } |
8 |
|
df-iun |
⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = { 𝑡 ∣ ∃ 𝑥 ∈ 𝐵 𝑡 ∈ 𝐶 } |
9 |
6 7 8
|
3eqtr4g |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 ) |
10 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 = 𝐷 ) |
11 |
10
|
iuneq2dv |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 ) |
12 |
9 11
|
eqtrd |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 ) |