Step |
Hyp |
Ref |
Expression |
1 |
|
rexeq |
⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ 𝑧 𝜓 ↔ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) |
2 |
1
|
abbidv |
⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ) |
3 |
2
|
eleq1d |
⊢ ( 𝑧 = 𝐴 → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) ) |
4 |
3
|
imbi2d |
⊢ ( 𝑧 = 𝐴 → ( ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ) ↔ ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) ) ) |
5 |
|
axrep6 |
⊢ ( ∀ 𝑥 ∃* 𝑦 𝜓 → ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) ) |
6 |
|
abbi |
⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) → { 𝑦 ∣ 𝑦 ∈ 𝑤 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ) |
7 |
|
abid2 |
⊢ { 𝑦 ∣ 𝑦 ∈ 𝑤 } = 𝑤 |
8 |
|
vex |
⊢ 𝑤 ∈ V |
9 |
7 8
|
eqeltri |
⊢ { 𝑦 ∣ 𝑦 ∈ 𝑤 } ∈ V |
10 |
6 9
|
eqeltrrdi |
⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ) |
11 |
10
|
exlimiv |
⊢ ( ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ) |
12 |
5 11
|
syl |
⊢ ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝑧 𝜓 } ∈ V ) |
13 |
4 12
|
vtoclg |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∃* 𝑦 𝜓 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) ) |
14 |
13
|
imp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∃* 𝑦 𝜓 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜓 } ∈ V ) |