Step |
Hyp |
Ref |
Expression |
1 |
|
ax-un |
⊢ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) |
2 |
|
eluni |
⊢ ( 𝑧 ∈ ∪ 𝑥 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) |
3 |
2
|
imbi1i |
⊢ ( ( 𝑧 ∈ ∪ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) |
4 |
3
|
albii |
⊢ ( ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) |
5 |
4
|
exbii |
⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ) |
6 |
1 5
|
mpbir |
⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 → 𝑧 ∈ 𝑦 ) |
7 |
6
|
bm1.3ii |
⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∪ 𝑥 ) |
8 |
|
dfcleq |
⊢ ( 𝑦 = ∪ 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∪ 𝑥 ) ) |
9 |
8
|
exbii |
⊢ ( ∃ 𝑦 𝑦 = ∪ 𝑥 ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∪ 𝑥 ) ) |
10 |
7 9
|
mpbir |
⊢ ∃ 𝑦 𝑦 = ∪ 𝑥 |