Step |
Hyp |
Ref |
Expression |
1 |
|
cover2g.1 |
⊢ 𝐴 = ∪ 𝐵 |
2 |
|
unieq |
⊢ ( 𝑏 = 𝐵 → ∪ 𝑏 = ∪ 𝐵 ) |
3 |
2 1
|
eqtr4di |
⊢ ( 𝑏 = 𝐵 → ∪ 𝑏 = 𝐴 ) |
4 |
|
rexeq |
⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) |
5 |
3 4
|
raleqbidv |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ ∪ 𝑏 ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ) |
6 |
|
pweq |
⊢ ( 𝑏 = 𝐵 → 𝒫 𝑏 = 𝒫 𝐵 ) |
7 |
3
|
eqeq2d |
⊢ ( 𝑏 = 𝐵 → ( ∪ 𝑧 = ∪ 𝑏 ↔ ∪ 𝑧 = 𝐴 ) ) |
8 |
7
|
anbi1d |
⊢ ( 𝑏 = 𝐵 → ( ( ∪ 𝑧 = ∪ 𝑏 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ↔ ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) ) |
9 |
6 8
|
rexeqbidv |
⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑧 ∈ 𝒫 𝑏 ( ∪ 𝑧 = ∪ 𝑏 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) ) |
10 |
|
vex |
⊢ 𝑏 ∈ V |
11 |
|
eqid |
⊢ ∪ 𝑏 = ∪ 𝑏 |
12 |
10 11
|
cover2 |
⊢ ( ∀ 𝑥 ∈ ∪ 𝑏 ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝑏 ( ∪ 𝑧 = ∪ 𝑏 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) |
13 |
5 9 12
|
vtoclbg |
⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) ) |