| Step | Hyp | Ref
| Expression |
| 1 | | nfrab1 3457 |
. . . 4
⊢
Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑} |
| 2 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑} |
| 3 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑧 𝐶 ∈ 𝐴 |
| 4 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 |
| 5 | 4 | nfel1 2922 |
. . . 4
⊢
Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 |
| 6 | | csbeq1a 3913 |
. . . . 5
⊢ (𝑦 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑦⦌𝐶) |
| 7 | 6 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝐶 ∈ 𝐴 ↔ ⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴)) |
| 8 | 1, 2, 3, 5, 7 | cbvralfw 3304 |
. . 3
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴) |
| 9 | | rabid 3458 |
. . . . . 6
⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑)) |
| 10 | 9 | imbi1i 349 |
. . . . 5
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴)) |
| 11 | | impexp 450 |
. . . . 5
⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴))) |
| 12 | 10, 11 | bitri 275 |
. . . 4
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴))) |
| 13 | 12 | ralbii2 3089 |
. . 3
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴)) |
| 14 | 8, 13 | bitr3i 277 |
. 2
⊢
(∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴)) |
| 15 | | rabn0 4389 |
. 2
⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅ ↔ ∃𝑦 ∈ 𝐵 𝜑) |
| 16 | | reusv2lem5 5402 |
. . 3
⊢
((∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)) |
| 17 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑧 𝑥 = 𝐶 |
| 18 | 4 | nfeq2 2923 |
. . . . . 6
⊢
Ⅎ𝑦 𝑥 = ⦋𝑧 / 𝑦⦌𝐶 |
| 19 | 6 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑧 / 𝑦⦌𝐶)) |
| 20 | 1, 2, 17, 18, 19 | cbvrexfw 3305 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶) |
| 21 | 9 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶)) |
| 22 | | anass 468 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶))) |
| 23 | 21, 22 | bitri 275 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶))) |
| 24 | 23 | rexbii2 3090 |
. . . . 5
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶)) |
| 25 | 20, 24 | bitr3i 277 |
. . . 4
⊢
(∃𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶)) |
| 26 | 25 | reubii 3389 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶)) |
| 27 | 1, 2, 17, 18, 19 | cbvralfw 3304 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶) |
| 28 | 9 | imbi1i 349 |
. . . . . . 7
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶)) |
| 29 | | impexp 450 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶))) |
| 30 | 28, 29 | bitri 275 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶))) |
| 31 | 30 | ralbii2 3089 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) |
| 32 | 27, 31 | bitr3i 277 |
. . . 4
⊢
(∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) |
| 33 | 32 | reubii 3389 |
. . 3
⊢
(∃!𝑥 ∈
𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) |
| 34 | 16, 26, 33 | 3bitr3g 313 |
. 2
⊢
((∀𝑧 ∈
{𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) |
| 35 | 14, 15, 34 | syl2anbr 599 |
1
⊢
((∀𝑦 ∈
𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) |