Proof of Theorem ceqsex6v
Step | Hyp | Ref
| Expression |
1 | | 3anass 1097 |
. . . . 5
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑))) |
2 | 1 | 3exbii 1857 |
. . . 4
⊢
(∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ ∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑))) |
3 | | 19.42vvv 1968 |
. . . 4
⊢
(∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑)) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑))) |
4 | 2, 3 | bitri 278 |
. . 3
⊢
(∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑))) |
5 | 4 | 3exbii 1857 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑))) |
6 | | ceqsex6v.1 |
. . . 4
⊢ 𝐴 ∈ V |
7 | | ceqsex6v.2 |
. . . 4
⊢ 𝐵 ∈ V |
8 | | ceqsex6v.3 |
. . . 4
⊢ 𝐶 ∈ V |
9 | | ceqsex6v.7 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
10 | 9 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ ((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜓))) |
11 | 10 | 3exbidv 1933 |
. . . 4
⊢ (𝑥 = 𝐴 → (∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜓))) |
12 | | ceqsex6v.8 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
13 | 12 | anbi2d 632 |
. . . . 5
⊢ (𝑦 = 𝐵 → (((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜓) ↔ ((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜒))) |
14 | 13 | 3exbidv 1933 |
. . . 4
⊢ (𝑦 = 𝐵 → (∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜓) ↔ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜒))) |
15 | | ceqsex6v.9 |
. . . . . 6
⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) |
16 | 15 | anbi2d 632 |
. . . . 5
⊢ (𝑧 = 𝐶 → (((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜒) ↔ ((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜃))) |
17 | 16 | 3exbidv 1933 |
. . . 4
⊢ (𝑧 = 𝐶 → (∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜒) ↔ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜃))) |
18 | 6, 7, 8, 11, 14, 17 | ceqsex3v 3460 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑)) ↔ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜃)) |
19 | | ceqsex6v.4 |
. . . 4
⊢ 𝐷 ∈ V |
20 | | ceqsex6v.5 |
. . . 4
⊢ 𝐸 ∈ V |
21 | | ceqsex6v.6 |
. . . 4
⊢ 𝐹 ∈ V |
22 | | ceqsex6v.10 |
. . . 4
⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏)) |
23 | | ceqsex6v.11 |
. . . 4
⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂)) |
24 | | ceqsex6v.12 |
. . . 4
⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁)) |
25 | 19, 20, 21, 22, 23, 24 | ceqsex3v 3460 |
. . 3
⊢
(∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜃) ↔ 𝜁) |
26 | 18, 25 | bitri 278 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ ∃𝑤∃𝑣∃𝑢((𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑)) ↔ 𝜁) |
27 | 5, 26 | bitri 278 |
1
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁) |