Step |
Hyp |
Ref |
Expression |
1 |
|
iineq12f.1 |
⊢ Ⅎ 𝑥 𝐴 |
2 |
|
iineq12f.2 |
⊢ Ⅎ 𝑥 𝐵 |
3 |
|
eleq2 |
⊢ ( 𝐶 = 𝐷 → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) |
4 |
3
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 → ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) ) |
5 |
|
ralbi |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐷 ) ) |
6 |
4 5
|
syl |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐷 ) ) |
7 |
1 2
|
raleqf |
⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐷 ↔ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 ) ) |
8 |
6 7
|
sylan9bbr |
⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 ) → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 ) ) |
9 |
8
|
abbidv |
⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 ) → { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 } ) |
10 |
|
df-iin |
⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 } |
11 |
|
df-iin |
⊢ ∩ 𝑥 ∈ 𝐵 𝐷 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 } |
12 |
9 10 11
|
3eqtr4g |
⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 ) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 ) |