Step | Hyp | Ref
| Expression |
1 | | nfrab1 3288 |
. . . 4
⊢
Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑} |
2 | | nfcv 2900 |
. . . 4
⊢
Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑} |
3 | | nfv 1921 |
. . . 4
⊢
Ⅎ𝑧 𝐶 ∈ 𝐴 |
4 | | nfcsb1v 3824 |
. . . . 5
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 |
5 | 4 | nfel1 2916 |
. . . 4
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 |
6 | | csbeq1a 3814 |
. . . . 5
⊢ (𝑦 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑦⦌𝐶) |
7 | 6 | eleq1d 2818 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝐶 ∈ 𝐴 ↔ ⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴)) |
8 | 1, 2, 3, 5, 7 | cbvralfw 3336 |
. . 3
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴) |
9 | | rabid 3282 |
. . . . . 6
⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑)) |
10 | 9 | imbi1i 353 |
. . . . 5
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴)) |
11 | | impexp 454 |
. . . . 5
⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴))) |
12 | 10, 11 | bitri 278 |
. . . 4
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴))) |
13 | 12 | ralbii2 3079 |
. . 3
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴)) |
14 | 8, 13 | bitr3i 280 |
. 2
⊢
(∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴)) |
15 | | rabn0 4284 |
. 2
⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅ ↔ ∃𝑦 ∈ 𝐵 𝜑) |
16 | | reusv2lem5 5279 |
. . 3
⊢
((∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)) |
17 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑧 𝑥 = 𝐶 |
18 | 4 | nfeq2 2917 |
. . . . . 6
⊢
Ⅎ𝑦 𝑥 = ⦋𝑧 / 𝑦⦌𝐶 |
19 | 6 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑧 / 𝑦⦌𝐶)) |
20 | 1, 2, 17, 18, 19 | cbvrexfw 3338 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶) |
21 | 9 | anbi1i 627 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶)) |
22 | | anass 472 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶))) |
23 | 21, 22 | bitri 278 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶))) |
24 | 23 | rexbii2 3160 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶)) |
25 | 20, 24 | bitr3i 280 |
. . . 4
⊢
(∃𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶)) |
26 | 25 | reubii 3295 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶)) |
27 | 1, 2, 17, 18, 19 | cbvralfw 3336 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶) |
28 | 9 | imbi1i 353 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶)) |
29 | | impexp 454 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶))) |
30 | 28, 29 | bitri 278 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶))) |
31 | 30 | ralbii2 3079 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) |
32 | 27, 31 | bitr3i 280 |
. . . 4
⊢
(∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) |
33 | 32 | reubii 3295 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) |
34 | 16, 26, 33 | 3bitr3g 316 |
. 2
⊢
((∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) |
35 | 14, 15, 34 | syl2anbr 602 |
1
⊢
((∀𝑦 ∈
𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) |