Step |
Hyp |
Ref |
Expression |
1 |
|
ralsng.1 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
df-ral |
⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝜑 ) ) |
3 |
|
velsn |
⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 ) |
4 |
3
|
imbi1i |
⊢ ( ( 𝑥 ∈ { 𝐴 } → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜑 ) ) |
5 |
4
|
albii |
⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) |
6 |
2 5
|
bitri |
⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) |
7 |
|
elisset |
⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 ) |
8 |
1
|
pm5.74i |
⊢ ( ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜓 ) ) |
9 |
8
|
albii |
⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ) |
10 |
9
|
a1i |
⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ) ) |
11 |
|
19.23v |
⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 ) ) |
12 |
11
|
a1i |
⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 ) ) ) |
13 |
|
pm5.5 |
⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 ) ↔ 𝜓 ) ) |
14 |
10 12 13
|
3bitrd |
⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) ) |
15 |
7 14
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ 𝜓 ) ) |
16 |
6 15
|
bitrid |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) ) |