Step |
Hyp |
Ref |
Expression |
1 |
|
moxfr.a |
⊢ 𝐴 ∈ V |
2 |
|
moxfr.b |
⊢ ∃! 𝑦 𝑥 = 𝐴 |
3 |
|
moxfr.c |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
4 |
1
|
a1i |
⊢ ( 𝑦 ∈ V → 𝐴 ∈ V ) |
5 |
|
euex |
⊢ ( ∃! 𝑦 𝑥 = 𝐴 → ∃ 𝑦 𝑥 = 𝐴 ) |
6 |
2 5
|
ax-mp |
⊢ ∃ 𝑦 𝑥 = 𝐴 |
7 |
|
rexv |
⊢ ( ∃ 𝑦 ∈ V 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑥 = 𝐴 ) |
8 |
6 7
|
mpbir |
⊢ ∃ 𝑦 ∈ V 𝑥 = 𝐴 |
9 |
8
|
a1i |
⊢ ( 𝑥 ∈ V → ∃ 𝑦 ∈ V 𝑥 = 𝐴 ) |
10 |
4 9 3
|
rexxfr |
⊢ ( ∃ 𝑥 ∈ V 𝜑 ↔ ∃ 𝑦 ∈ V 𝜓 ) |
11 |
|
rexv |
⊢ ( ∃ 𝑥 ∈ V 𝜑 ↔ ∃ 𝑥 𝜑 ) |
12 |
|
rexv |
⊢ ( ∃ 𝑦 ∈ V 𝜓 ↔ ∃ 𝑦 𝜓 ) |
13 |
10 11 12
|
3bitr3i |
⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) |
14 |
1 2 3
|
euxfrw |
⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 ) |
15 |
13 14
|
imbi12i |
⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 𝜓 → ∃! 𝑦 𝜓 ) ) |
16 |
|
moeu |
⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ) |
17 |
|
moeu |
⊢ ( ∃* 𝑦 𝜓 ↔ ( ∃ 𝑦 𝜓 → ∃! 𝑦 𝜓 ) ) |
18 |
15 16 17
|
3bitr4i |
⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 ) |