Proof of Theorem ceqsex6v
Step | Hyp | Ref
| Expression |
1 | | 3anass 888 |
. . . . 5
⊢
(((x = A ∧ y = B ∧ z = 𝐶) ∧ (w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔
((x = A
∧ y =
B ∧
z = 𝐶) ∧
((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ))) |
2 | 1 | 3exbii 1495 |
. . . 4
⊢ (∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧
(w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧
((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ))) |
3 | | 19.42vvv 1786 |
. . . 4
⊢ (∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧
((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)) ↔ ((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ))) |
4 | 2, 3 | bitri 173 |
. . 3
⊢ (∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧
(w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ))) |
5 | 4 | 3exbii 1495 |
. 2
⊢ (∃x∃y∃z∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧
(w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ∃x∃y∃z((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ))) |
6 | | ceqsex6v.1 |
. . . 4
⊢ A ∈
V |
7 | | ceqsex6v.2 |
. . . 4
⊢ B ∈
V |
8 | | ceqsex6v.3 |
. . . 4
⊢ 𝐶 ∈ V |
9 | | ceqsex6v.7 |
. . . . . 6
⊢ (x = A →
(φ ↔ ψ)) |
10 | 9 | anbi2d 437 |
. . . . 5
⊢ (x = A →
(((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ))) |
11 | 10 | 3exbidv 1746 |
. . . 4
⊢ (x = A →
(∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ))) |
12 | | ceqsex6v.8 |
. . . . . 6
⊢ (y = B →
(ψ ↔ χ)) |
13 | 12 | anbi2d 437 |
. . . . 5
⊢ (y = B →
(((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ) ↔ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ))) |
14 | 13 | 3exbidv 1746 |
. . . 4
⊢ (y = B →
(∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ ψ) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ))) |
15 | | ceqsex6v.9 |
. . . . . 6
⊢ (z = 𝐶 → (χ ↔ θ)) |
16 | 15 | anbi2d 437 |
. . . . 5
⊢ (z = 𝐶 → (((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ) ↔ ((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ))) |
17 | 16 | 3exbidv 1746 |
. . . 4
⊢ (z = 𝐶 → (∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ χ) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ))) |
18 | 6, 7, 8, 11, 14, 17 | ceqsex3v 2590 |
. . 3
⊢ (∃x∃y∃z((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)) ↔ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ)) |
19 | | ceqsex6v.4 |
. . . 4
⊢ 𝐷 ∈ V |
20 | | ceqsex6v.5 |
. . . 4
⊢ 𝐸 ∈ V |
21 | | ceqsex6v.6 |
. . . 4
⊢ 𝐹 ∈ V |
22 | | ceqsex6v.10 |
. . . 4
⊢ (w = 𝐷 → (θ ↔ τ)) |
23 | | ceqsex6v.11 |
. . . 4
⊢ (v = 𝐸 → (τ ↔ η)) |
24 | | ceqsex6v.12 |
. . . 4
⊢ (u = 𝐹 → (η ↔ ζ)) |
25 | 19, 20, 21, 22, 23, 24 | ceqsex3v 2590 |
. . 3
⊢ (∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ θ) ↔ ζ) |
26 | 18, 25 | bitri 173 |
. 2
⊢ (∃x∃y∃z((x = A ∧ y = B ∧ z = 𝐶) ∧ ∃w∃v∃u((w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ)) ↔ ζ) |
27 | 5, 26 | bitri 173 |
1
⊢ (∃x∃y∃z∃w∃v∃u((x = A ∧ y = B ∧ z = 𝐶) ∧
(w = 𝐷 ∧ v = 𝐸 ∧ u = 𝐹) ∧ φ) ↔ ζ) |