Step |
Hyp |
Ref |
Expression |
1 |
|
reu8nf.1 |
⊢ Ⅎ 𝑥 𝜓 |
2 |
|
reu8nf.2 |
⊢ Ⅎ 𝑥 𝜒 |
3 |
|
reu8nf.3 |
⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) ) |
4 |
|
reu8nf.4 |
⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) ) |
5 |
|
nfv |
⊢ Ⅎ 𝑤 𝜑 |
6 |
5 2 3
|
cbvreuw |
⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑤 ∈ 𝐴 𝜒 ) |
7 |
4
|
reu8 |
⊢ ( ∃! 𝑤 ∈ 𝐴 𝜒 ↔ ∃ 𝑤 ∈ 𝐴 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ) |
8 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐴 |
9 |
|
nfv |
⊢ Ⅎ 𝑥 𝑤 = 𝑦 |
10 |
1 9
|
nfim |
⊢ Ⅎ 𝑥 ( 𝜓 → 𝑤 = 𝑦 ) |
11 |
8 10
|
nfralw |
⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) |
12 |
2 11
|
nfan |
⊢ Ⅎ 𝑥 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) |
13 |
|
nfv |
⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) |
14 |
3
|
bicomd |
⊢ ( 𝑥 = 𝑤 → ( 𝜒 ↔ 𝜑 ) ) |
15 |
14
|
equcoms |
⊢ ( 𝑤 = 𝑥 → ( 𝜒 ↔ 𝜑 ) ) |
16 |
|
equequ1 |
⊢ ( 𝑤 = 𝑥 → ( 𝑤 = 𝑦 ↔ 𝑥 = 𝑦 ) ) |
17 |
16
|
imbi2d |
⊢ ( 𝑤 = 𝑥 → ( ( 𝜓 → 𝑤 = 𝑦 ) ↔ ( 𝜓 → 𝑥 = 𝑦 ) ) ) |
18 |
17
|
ralbidv |
⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) |
19 |
15 18
|
anbi12d |
⊢ ( 𝑤 = 𝑥 → ( ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) ) |
20 |
12 13 19
|
cbvrexw |
⊢ ( ∃ 𝑤 ∈ 𝐴 ( 𝜒 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑤 = 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) |
21 |
6 7 20
|
3bitri |
⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑦 ) ) ) |