Step | Hyp | Ref
| Expression |
1 | | eqidd 2738 |
. . . . 5
⊢ (𝜓 → 𝐶 = 𝐶) |
2 | 1 | ancli 552 |
. . . 4
⊢ (𝜓 → (𝜓 ∧ 𝐶 = 𝐶)) |
3 | | unirep.1 |
. . . . . 6
⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓)) |
4 | | unirep.2 |
. . . . . . 7
⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶) |
5 | 4 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑦 = 𝐷 → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶)) |
6 | 3, 5 | anbi12d 634 |
. . . . 5
⊢ (𝑦 = 𝐷 → ((𝜑 ∧ 𝐶 = 𝐵) ↔ (𝜓 ∧ 𝐶 = 𝐶))) |
7 | 6 | rspcev 3537 |
. . . 4
⊢ ((𝐷 ∈ 𝐴 ∧ (𝜓 ∧ 𝐶 = 𝐶)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)) |
8 | 2, 7 | sylan2 596 |
. . 3
⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)) |
9 | 8 | adantl 485 |
. 2
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)) |
10 | | nfcvd 2905 |
. . . . . 6
⊢ (𝐷 ∈ 𝐴 → Ⅎ𝑦𝐶) |
11 | 10, 4 | csbiegf 3845 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → ⦋𝐷 / 𝑦⦌𝐵 = 𝐶) |
12 | | unirep.5 |
. . . . . 6
⊢ 𝐵 ∈ V |
13 | 12 | csbex 5204 |
. . . . 5
⊢
⦋𝐷 /
𝑦⦌𝐵 ∈ V |
14 | 11, 13 | eqeltrrdi 2847 |
. . . 4
⊢ (𝐷 ∈ 𝐴 → 𝐶 ∈ V) |
15 | 14 | ad2antrl 728 |
. . 3
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → 𝐶 ∈ V) |
16 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐶 → (𝑥 = 𝐵 ↔ 𝐶 = 𝐵)) |
17 | 16 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐶 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝐶 = 𝐵))) |
18 | 17 | rexbidv 3216 |
. . . . . . . . 9
⊢ (𝑥 = 𝐶 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))) |
19 | 18 | spcegv 3512 |
. . . . . . . 8
⊢ (𝐶 ∈ V → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))) |
20 | 14, 19 | syl 17 |
. . . . . . 7
⊢ (𝐷 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))) |
21 | 20 | adantr 484 |
. . . . . 6
⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))) |
22 | 8, 21 | mpd 15 |
. . . . 5
⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) |
23 | 22 | adantl 485 |
. . . 4
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) |
24 | | r19.29 3176 |
. . . . . . . 8
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵))) |
25 | | r19.29 3176 |
. . . . . . . . . . . 12
⊢
((∀𝑧 ∈
𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → ∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹))) |
26 | | an4 656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹))) |
27 | | pm3.35 803 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → 𝐵 = 𝐹) |
28 | | eqeq12 2754 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → (𝑥 = 𝑤 ↔ 𝐵 = 𝐹)) |
29 | 27, 28 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤)) |
30 | 29 | ancoms 462 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝜒)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤)) |
31 | 30 | expimpd 457 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)) |
32 | 26, 31 | syl5bi 245 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)) |
33 | 32 | ancomsd 469 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜒 ∧ 𝑤 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)) |
34 | 33 | expdimp 456 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤)) |
35 | 34 | rexlimivw 3201 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤)) |
36 | 35 | imp 410 |
. . . . . . . . . . . 12
⊢
((∃𝑧 ∈
𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤) |
37 | 25, 36 | sylan 583 |
. . . . . . . . . . 11
⊢
(((∀𝑧 ∈
𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤) |
38 | 37 | an32s 652 |
. . . . . . . . . 10
⊢
(((∀𝑧 ∈
𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤) |
39 | 38 | ex 416 |
. . . . . . . . 9
⊢
((∀𝑧 ∈
𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤)) |
40 | 39 | rexlimivw 3201 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤)) |
41 | 24, 40 | syl 17 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤)) |
42 | 41 | expimpd 457 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)) |
43 | 42 | adantr 484 |
. . . . 5
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)) |
44 | 43 | alrimivv 1936 |
. . . 4
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)) |
45 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 = 𝐵 ↔ 𝑤 = 𝐵)) |
46 | 45 | anbi2d 632 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝑤 = 𝐵))) |
47 | 46 | rexbidv 3216 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵))) |
48 | | unirep.3 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) |
49 | | unirep.4 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹) |
50 | 49 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑤 = 𝐵 ↔ 𝑤 = 𝐹)) |
51 | 48, 50 | anbi12d 634 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑤 = 𝐵) ↔ (𝜒 ∧ 𝑤 = 𝐹))) |
52 | 51 | cbvrexvw 3359 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐴 (𝜑 ∧ 𝑤 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) |
53 | 47, 52 | bitrdi 290 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹))) |
54 | 53 | eu4 2616 |
. . . 4
⊢
(∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))) |
55 | 23, 44, 54 | sylanbrc 586 |
. . 3
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) |
56 | 18 | iota2 6369 |
. . 3
⊢ ((𝐶 ∈ V ∧ ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)) |
57 | 15, 55, 56 | syl2anc 587 |
. 2
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)) |
58 | 9, 57 | mpbid 235 |
1
⊢
((∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶) |