Proof of Theorem eqvincg
Step | Hyp | Ref
| Expression |
1 | | elisset 2738 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
2 | | ax-1 6 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐴 = 𝐵 → 𝑥 = 𝐴)) |
3 | | eqtr 2182 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝐴 = 𝐵) → 𝑥 = 𝐵) |
4 | 3 | ex 114 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐴 = 𝐵 → 𝑥 = 𝐵)) |
5 | 2, 4 | jca 304 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵))) |
6 | 5 | eximi 1587 |
. . . 4
⊢
(∃𝑥 𝑥 = 𝐴 → ∃𝑥((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵))) |
7 | | pm3.43 592 |
. . . . 5
⊢ (((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵)) → (𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
8 | 7 | eximi 1587 |
. . . 4
⊢
(∃𝑥((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵)) → ∃𝑥(𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
9 | 1, 6, 8 | 3syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
10 | | nfv 1515 |
. . . 4
⊢
Ⅎ𝑥 𝐴 = 𝐵 |
11 | 10 | 19.37-1 1661 |
. . 3
⊢
(∃𝑥(𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) → (𝐴 = 𝐵 → ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
12 | 9, 11 | syl 14 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |
13 | | eqtr2 2183 |
. . 3
⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → 𝐴 = 𝐵) |
14 | 13 | exlimiv 1585 |
. 2
⊢
(∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → 𝐴 = 𝐵) |
15 | 12, 14 | impbid1 141 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))) |