Step |
Hyp |
Ref |
Expression |
1 |
|
2eu1 |
⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) ) |
2 |
1
|
pm5.32ri |
⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ) |
3 |
|
eumo |
⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 ) |
4 |
3
|
adantl |
⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃* 𝑦 ∃ 𝑥 𝜑 ) |
5 |
|
2moex |
⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ∀ 𝑥 ∃* 𝑦 𝜑 ) |
6 |
4 5
|
syl |
⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∀ 𝑥 ∃* 𝑦 𝜑 ) |
7 |
6
|
pm4.71i |
⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ) |
8 |
|
2eu4 |
⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) |
9 |
2 7 8
|
3bitr2i |
⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) |