Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴)) → 𝑦 = [𝑥](𝐴 × 𝐴)) |
2 | | ecxpid 30925 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → [𝑥](𝐴 × 𝐴) = 𝐴) |
3 | 2 | adantr 483 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴)) → [𝑥](𝐴 × 𝐴) = 𝐴) |
4 | 1, 3 | eqtrd 2856 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴)) → 𝑦 = 𝐴) |
5 | 4 | rexlimiva 3281 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 = [𝑥](𝐴 × 𝐴) → 𝑦 = 𝐴) |
6 | 5 | adantl 484 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥](𝐴 × 𝐴)) → 𝑦 = 𝐴) |
7 | | n0 4310 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
8 | 7 | biimpi 218 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
∃𝑥 𝑥 ∈ 𝐴) |
9 | | simpl 485 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑦 = 𝐴) |
10 | 2 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝐴) → [𝑥](𝐴 × 𝐴) = 𝐴) |
11 | 9, 10 | eqtr4d 2859 |
. . . . . . . . 9
⊢ ((𝑦 = 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑦 = [𝑥](𝐴 × 𝐴)) |
12 | 11 | ex 415 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝐴 → 𝑦 = [𝑥](𝐴 × 𝐴))) |
13 | 12 | ancld 553 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴)))) |
14 | 13 | eximdv 1918 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴)))) |
15 | 8, 14 | mpan9 509 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝑦 = 𝐴) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴))) |
16 | | df-rex 3144 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 = [𝑥](𝐴 × 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = [𝑥](𝐴 × 𝐴))) |
17 | 15, 16 | sylibr 236 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝑦 = 𝐴) → ∃𝑥 ∈ 𝐴 𝑦 = [𝑥](𝐴 × 𝐴)) |
18 | 6, 17 | impbida 799 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∃𝑥 ∈ 𝐴 𝑦 = [𝑥](𝐴 × 𝐴) ↔ 𝑦 = 𝐴)) |
19 | | vex 3497 |
. . . 4
⊢ 𝑦 ∈ V |
20 | 19 | elqs 8349 |
. . 3
⊢ (𝑦 ∈ (𝐴 / (𝐴 × 𝐴)) ↔ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥](𝐴 × 𝐴)) |
21 | | velsn 4583 |
. . 3
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
22 | 18, 20, 21 | 3bitr4g 316 |
. 2
⊢ (𝐴 ≠ ∅ → (𝑦 ∈ (𝐴 / (𝐴 × 𝐴)) ↔ 𝑦 ∈ {𝐴})) |
23 | 22 | eqrdv 2819 |
1
⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴}) |