Step |
Hyp |
Ref |
Expression |
1 |
|
elequ2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) |
2 |
1
|
anbi1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 ∈ 𝑥 ∧ 𝜒 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝜒 ) ) ) |
3 |
2
|
exbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑤 ( 𝑧 ∈ 𝑥 ∧ 𝜒 ) ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑦 ∧ 𝜒 ) ) ) |
4 |
3
|
bibi2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑦 ∧ 𝜒 ) ) ) ) |
5 |
4
|
albidv |
⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑣 ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ∀ 𝑣 ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑦 ∧ 𝜒 ) ) ) ) |
6 |
5
|
imbi2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ∀ 𝑣 ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑥 ∧ 𝜒 ) ) ) ↔ ( 𝜑 → ∀ 𝑣 ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑦 ∧ 𝜒 ) ) ) ) ) |
7 |
6
|
exbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑢 ( 𝜑 → ∀ 𝑣 ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑥 ∧ 𝜒 ) ) ) ↔ ∃ 𝑢 ( 𝜑 → ∀ 𝑣 ( 𝜓 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑦 ∧ 𝜒 ) ) ) ) ) |