Step | Hyp | Ref
| Expression |
1 | | 2reu8i.w |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒)) |
2 | 1 | reu8 3614 |
. . . 4
⊢
(∃!𝑦 ∈
𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤))) |
3 | 2 | reubii 3316 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤))) |
4 | | 2reu8i.x |
. . . . . 6
⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏)) |
5 | | 2reu8i.v |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃)) |
6 | 5 | imbi1d 333 |
. . . . . . 7
⊢ (𝑥 = 𝑣 → ((𝜒 → 𝑦 = 𝑤) ↔ (𝜃 → 𝑦 = 𝑤))) |
7 | 6 | ralbidv 3168 |
. . . . . 6
⊢ (𝑥 = 𝑣 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤))) |
8 | 4, 7 | anbi12d 624 |
. . . . 5
⊢ (𝑥 = 𝑣 → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)))) |
9 | 8 | rexbidv 3237 |
. . . 4
⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)))) |
10 | 9 | reu8 3614 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣))) |
11 | 3, 10 | bitri 267 |
. 2
⊢
(∃!𝑥 ∈
𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣))) |
12 | | nfv 1957 |
. . . . . . . . 9
⊢
Ⅎ𝑢(𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) |
13 | | nfs1v 2254 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[𝑢 / 𝑦]𝜏 |
14 | | nfcv 2934 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝐵 |
15 | | nfs1v 2254 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦[𝑢 / 𝑦]𝜃 |
16 | | nfv 1957 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑢 = 𝑤 |
17 | 15, 16 | nfim 1943 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) |
18 | 14, 17 | nfral 3127 |
. . . . . . . . . 10
⊢
Ⅎ𝑦∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) |
19 | 13, 18 | nfan 1946 |
. . . . . . . . 9
⊢
Ⅎ𝑦([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) |
20 | | sbequ12 2229 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑢 → (𝜏 ↔ [𝑢 / 𝑦]𝜏)) |
21 | | sbequ12 2229 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑢 → (𝜃 ↔ [𝑢 / 𝑦]𝜃)) |
22 | | equequ1 2072 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑢 → (𝑦 = 𝑤 ↔ 𝑢 = 𝑤)) |
23 | 21, 22 | imbi12d 336 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑢 → ((𝜃 → 𝑦 = 𝑤) ↔ ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))) |
24 | 23 | ralbidv 3168 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑢 → (∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))) |
25 | 20, 24 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑦 = 𝑢 → ((𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))) |
26 | 12, 19, 25 | cbvrex 3364 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))) |
27 | 26 | imbi1i 341 |
. . . . . . 7
⊢
((∃𝑦 ∈
𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) |
28 | 27 | ralbii 3162 |
. . . . . 6
⊢
(∀𝑣 ∈
𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣) ↔ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) |
29 | 28 | anbi2i 616 |
. . . . 5
⊢
((∃𝑦 ∈
𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) |
30 | | nfcv 2934 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
31 | 14, 19 | nfrex 3188 |
. . . . . . . 8
⊢
Ⅎ𝑦∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) |
32 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑥 = 𝑣 |
33 | 31, 32 | nfim 1943 |
. . . . . . 7
⊢
Ⅎ𝑦(∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) |
34 | 30, 33 | nfral 3127 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) |
35 | 34 | r19.41 3276 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) |
36 | 29, 35 | bitr4i 270 |
. . . 4
⊢
((∃𝑦 ∈
𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) ↔ ∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) |
37 | | r19.28v 3257 |
. . . . . . . . 9
⊢
((∀𝑤 ∈
𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) |
38 | | simplr 759 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → 𝜑) |
39 | | nfv 1957 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑣∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) |
40 | | nfcv 2934 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑣𝐵 |
41 | | nfs1v 2254 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜏 |
42 | | nfs1v 2254 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑣[𝑎 / 𝑣][𝑢 / 𝑦]𝜃 |
43 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑣 𝑢 = 𝑤 |
44 | 42, 43 | nfim 1943 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) |
45 | 40, 44 | nfral 3127 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑣∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) |
46 | 41, 45 | nfan 1946 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑣([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) |
47 | 40, 46 | nfrex 3188 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑣∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) |
48 | | nfv 1957 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑣 𝑥 = 𝑎 |
49 | 47, 48 | nfim 1943 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑣(∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) |
50 | 39, 49 | nfan 1946 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑣(∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) |
51 | | sbequ12 2229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜏)) |
52 | | sbequ12 2229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = 𝑎 → ([𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑢 / 𝑦]𝜃)) |
53 | 52 | imbi1d 333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))) |
54 | 53 | ralbidv 3168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑎 → (∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))) |
55 | 51, 54 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑎 → (([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))) |
56 | 55 | rexbidv 3237 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑎 → (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)))) |
57 | | equequ2 2073 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑎 → (𝑥 = 𝑣 ↔ 𝑥 = 𝑎)) |
58 | 56, 57 | imbi12d 336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑎 → ((∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) ↔ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎))) |
59 | 58 | anbi2d 622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑎 → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) ↔ (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)))) |
60 | 50, 59 | rspc 3505 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ 𝐴 → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)))) |
61 | 60 | ad2antrl 718 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)))) |
62 | | nfs1v 2254 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤[𝑏 / 𝑤]𝜒 |
63 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤 𝑦 = 𝑏 |
64 | 62, 63 | nfim 1943 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) |
65 | | sbequ12 2229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑏 → (𝜒 ↔ [𝑏 / 𝑤]𝜒)) |
66 | | equequ2 2073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑏 → (𝑦 = 𝑤 ↔ 𝑦 = 𝑏)) |
67 | 65, 66 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑏 → ((𝜒 → 𝑦 = 𝑤) ↔ ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))) |
68 | 64, 67 | rspc 3505 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))) |
69 | 68 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))) |
70 | 69 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏))) |
71 | 70 | imp 397 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏)) |
72 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦𝜒 |
73 | 72, 1 | sbiev 2286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑤 / 𝑦]𝜑 ↔ 𝜒) |
74 | 73 | bicomi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 ↔ [𝑤 / 𝑦]𝜑) |
75 | 74 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑤][𝑤 / 𝑦]𝜑) |
76 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤𝜑 |
77 | 76 | sbco2 2492 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑏 / 𝑤][𝑤 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑) |
78 | 75, 77 | bitri 267 |
. . . . . . . . . . . . . . . . . 18
⊢ ([𝑏 / 𝑤]𝜒 ↔ [𝑏 / 𝑦]𝜑) |
79 | 78 | imbi1i 341 |
. . . . . . . . . . . . . . . . 17
⊢ (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) ↔ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) |
80 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑦𝜂 |
81 | | 2reu8i.b |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂)) |
82 | 80, 81 | sbie 2484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑏 / 𝑦]𝜑 ↔ 𝜂) |
83 | | pm3.35 793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑦 = 𝑏) |
84 | 83 | equcomd 2066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (([𝑏 / 𝑦]𝜑 ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → 𝑏 = 𝑦) |
85 | 84 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑏 / 𝑦]𝜑 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦)) |
86 | 82, 85 | sylbir 227 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜂 → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑏 = 𝑦)) |
87 | 86 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝜂 → 𝑏 = 𝑦)) |
88 | 87 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → 𝑏 = 𝑦)) |
89 | | simplrr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → 𝑏 ∈ 𝐵) |
90 | 89 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → 𝑏 ∈ 𝐵) |
91 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑥 𝑢 = 𝑏 |
92 | | sbequ 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = 𝑏 → ([𝑢 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)) |
93 | 91, 92 | sbbid 2227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝑏 → ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)) |
94 | | equequ1 2072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 = 𝑏 → (𝑢 = 𝑤 ↔ 𝑏 = 𝑤)) |
95 | 94 | imbi2d 332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))) |
96 | 95 | ralbidv 3168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝑏 → (∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))) |
97 | 93, 96 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝑏 → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))) |
98 | 97 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) ∧ 𝑢 = 𝑏) → (([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)))) |
99 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑎 ∈ V |
100 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑏 ∈ V |
101 | | 2reu8i.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓)) |
102 | 99, 100, 101 | sbc2ie 3723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓) |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜓)) |
104 | 103 | biimprd 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝜓 → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)) |
105 | 104 | adantld 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → ((𝜂 ∧ 𝜓) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑)) |
106 | 105 | imp 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑) |
107 | | sbsbc 3656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ([𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑) |
108 | 107 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑) |
109 | | sbsbc 3656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑) |
110 | 108, 109 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑏 / 𝑦]𝜑) |
111 | 106, 110 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → [𝑎 / 𝑥][𝑏 / 𝑦]𝜑) |
112 | 72, 1 | sbie 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ([𝑤 / 𝑦]𝜑 ↔ 𝜒) |
113 | 112 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑎 / 𝑥]𝜒) |
114 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑥𝜁 |
115 | | 2reu8i.a |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁)) |
116 | 114, 115 | sbie 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ([𝑎 / 𝑥]𝜒 ↔ 𝜁) |
117 | 113, 116 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 ↔ 𝜁) |
118 | | 2reu8i.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤) |
119 | 118 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜒 → 𝑦 = 𝑤) → (𝜁 → 𝑦 = 𝑤)) |
120 | 119 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑦 = 𝑤)) |
121 | 82 | imbi1i 341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) ↔ (𝜂 → 𝑦 = 𝑏)) |
122 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜂 → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏)) |
123 | 122 | ad2antrl 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → ((𝜂 → 𝑦 = 𝑏) → 𝑦 = 𝑏)) |
124 | 121, 123 | syl5bi 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → 𝑦 = 𝑏)) |
125 | | ax7 2063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 = 𝑏 → (𝑦 = 𝑤 → 𝑏 = 𝑤)) |
126 | 124, 125 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (𝑦 = 𝑤 → 𝑏 = 𝑤))) |
127 | 126 | imp 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (𝑦 = 𝑤 → 𝑏 = 𝑤)) |
128 | 127 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝑦 = 𝑤 → 𝑏 = 𝑤)) |
129 | 120, 128 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → (𝜁 → 𝑏 = 𝑤)) |
130 | 117, 129 | syl5bi 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) ∧ (𝜒 → 𝑦 = 𝑤)) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)) |
131 | 130 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ 𝑤 ∈ 𝐵) → ((𝜒 → 𝑦 = 𝑤) → ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))) |
132 | 131 | ralimdva 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝜂 ∧ 𝜓)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))) |
133 | 132 | exp31 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝜂 ∧ 𝜓) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))) |
134 | 133 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((𝜂 ∧ 𝜓) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))))) |
135 | 134 | imp41 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤)) |
136 | 111, 135 | jca 507 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑏 = 𝑤))) |
137 | 90, 98, 136 | rspcedvd 3518 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))) |
138 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
Ⅎ𝑥𝜏 |
139 | 138, 4 | sbiev 2286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ([𝑣 / 𝑥]𝜑 ↔ 𝜏) |
140 | 139 | bicomi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜏 ↔ [𝑣 / 𝑥]𝜑) |
141 | 140 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜑) |
142 | | sbcom2 2523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜑 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑) |
143 | 141, 142 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ([𝑢 / 𝑦]𝜏 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜑) |
144 | 143 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑) |
145 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑣[𝑢 / 𝑦]𝜑 |
146 | 145 | sbco2 2492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑) |
147 | 144, 146 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜑) |
148 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
Ⅎ𝑥𝜃 |
149 | 148, 5 | sbiev 2286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ([𝑣 / 𝑥]𝜒 ↔ 𝜃) |
150 | 149 | bicomi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜃 ↔ [𝑣 / 𝑥]𝜒) |
151 | 150 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑢 / 𝑦][𝑣 / 𝑥]𝜒) |
152 | | sbcom2 2523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ([𝑢 / 𝑦][𝑣 / 𝑥]𝜒 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒) |
153 | 151, 152 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ([𝑢 / 𝑦]𝜃 ↔ [𝑣 / 𝑥][𝑢 / 𝑦]𝜒) |
154 | 153 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒) |
155 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
Ⅎ𝑣[𝑢 / 𝑦]𝜒 |
156 | 155 | sbco2 2492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ([𝑎 / 𝑣][𝑣 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑢 / 𝑦]𝜒) |
157 | 74 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑢 / 𝑦][𝑤 / 𝑦]𝜑) |
158 | | nfs1v 2254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜑 |
159 | 158 | sbf 2456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ([𝑢 / 𝑦][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦]𝜑) |
160 | 157, 159 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ([𝑢 / 𝑦]𝜒 ↔ [𝑤 / 𝑦]𝜑) |
161 | 160 | sbbii 2019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜒 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑) |
162 | 154, 156,
161 | 3bitri 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 ↔ [𝑎 / 𝑥][𝑤 / 𝑦]𝜑) |
163 | 162 | imbi1i 341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) |
164 | 163 | ralbii 3162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑤 ∈
𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤) ↔ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤)) |
165 | 147, 164 | anbi12i 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))) |
166 | 165 | rexbii 3224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃𝑢 ∈
𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) ↔ ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑥][𝑢 / 𝑦]𝜑 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑥][𝑤 / 𝑦]𝜑 → 𝑢 = 𝑤))) |
167 | 137, 166 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤))) |
168 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∃𝑢 ∈
𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎)) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (𝜂 ∧ 𝜓)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → 𝑥 = 𝑎)) |
170 | 169 | impancom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → ((𝜂 ∧ 𝜓) → 𝑥 = 𝑎)) |
171 | 170 | imp 397 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑥 = 𝑎) |
172 | 171 | equcomd 2066 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) ∧ (𝜂 ∧ 𝜓)) → 𝑎 = 𝑥) |
173 | 172 | exp32 413 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝜓 → 𝑎 = 𝑥))) |
174 | 88, 173 | jcad 508 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑥 ∈
𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏)) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))) |
175 | 174 | exp31 412 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑦]𝜑 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
176 | 79, 175 | syl5bi 234 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (([𝑏 / 𝑤]𝜒 → 𝑦 = 𝑏) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
177 | 71, 176 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → ((∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |
178 | 177 | expimpd 447 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑎 / 𝑣][𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑎)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |
179 | 61, 178 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |
180 | 179 | impancom 445 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |
181 | 180 | ralrimivv 3152 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))) |
182 | 38, 181 | jca 507 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) ∧ ∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣))) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |
183 | 182 | ex 403 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑣 ∈ 𝐴 (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
184 | 37, 183 | syl5 34 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ((∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
185 | 184 | expd 406 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))) |
186 | 185 | expimpd 447 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) → (∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))))) |
187 | 186 | impd 400 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
188 | 187 | reximdva 3198 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ((𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑢 ∈ 𝐵 ([𝑢 / 𝑦]𝜏 ∧ ∀𝑤 ∈ 𝐵 ([𝑢 / 𝑦]𝜃 → 𝑢 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
189 | 36, 188 | syl5bi 234 |
. . 3
⊢ (𝑥 ∈ 𝐴 → ((∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥)))))) |
190 | 189 | reximia 3190 |
. 2
⊢
(∃𝑥 ∈
𝐴 (∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑤 ∈ 𝐵 (𝜒 → 𝑦 = 𝑤)) ∧ ∀𝑣 ∈ 𝐴 (∃𝑦 ∈ 𝐵 (𝜏 ∧ ∀𝑤 ∈ 𝐵 (𝜃 → 𝑦 = 𝑤)) → 𝑥 = 𝑣)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |
191 | 11, 190 | sylbi 209 |
1
⊢
(∃!𝑥 ∈
𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) |