Step | Hyp | Ref
| Expression |
1 | | elex 2566 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | elex 2566 |
. 2
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
3 | | elex 2566 |
. 2
⊢ (𝐶 ∈ 𝑋 → 𝐶 ∈ V) |
4 | | opexg 3964 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 ∈ V) |
5 | | opexg 3964 |
. . . . 5
⊢
((〈𝐴, 𝐵〉 ∈ V ∧ 𝐶 ∈ V) →
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V) |
6 | 4, 5 | sylan 267 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V) →
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V) |
7 | 6 | 3impa 1099 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) →
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V) |
8 | | simpr 103 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) |
9 | 8 | eqeq1d 2048 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
10 | | eqcom 2042 |
. . . . . . . . . . 11
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝐴, 𝐵〉, 𝐶〉) |
11 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
13 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
14 | 11, 12, 13 | otth2 3978 |
. . . . . . . . . . 11
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
15 | 10, 14 | bitri 173 |
. . . . . . . . . 10
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
16 | 9, 15 | syl6bb 185 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶))) |
17 | 16 | anbi1d 438 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑))) |
18 | | eloprabga.1 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) |
19 | 18 | pm5.32i 427 |
. . . . . . . 8
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓)) |
20 | 17, 19 | syl6bb 185 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
21 | 20 | 3exbidv 1749 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
22 | | df-oprab 5516 |
. . . . . . . . . 10
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
23 | 22 | eleq2i 2104 |
. . . . . . . . 9
⊢ (𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝑤 ∈ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)}) |
24 | | abid 2028 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
25 | 23, 24 | bitr2i 174 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) |
26 | | eleq1 2100 |
. . . . . . . 8
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → (𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
27 | 25, 26 | syl5bb 181 |
. . . . . . 7
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
28 | 27 | adantl 262 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
29 | | elisset 2568 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴) |
30 | | elisset 2568 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → ∃𝑦 𝑦 = 𝐵) |
31 | | elisset 2568 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ V → ∃𝑧 𝑧 = 𝐶) |
32 | 29, 30, 31 | 3anim123i 1089 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
33 | | eeeanv 1808 |
. . . . . . . . . 10
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
34 | 32, 33 | sylibr 137 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → ∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
35 | 34 | biantrurd 289 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝜓 ↔ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
36 | | 19.41vvv 1784 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓)) |
37 | 35, 36 | syl6rbbr 188 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓)) |
38 | 37 | adantr 261 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓)) |
39 | 21, 28, 38 | 3bitr3d 207 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
40 | 39 | expcom 109 |
. . . 4
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓))) |
41 | 40 | vtocleg 2624 |
. . 3
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 ∈ V → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓))) |
42 | 7, 41 | mpcom 32 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) →
(〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
43 | 1, 2, 3, 42 | syl3an 1177 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |