Step | Hyp | Ref
| Expression |
1 | | elex 3440 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | elex 3440 |
. 2
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
3 | | elex 3440 |
. 2
⊢ (𝐶 ∈ 𝑋 → 𝐶 ∈ V) |
4 | | opex 5373 |
. . 3
⊢
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V |
5 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) |
6 | 5 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
7 | | eqcom 2745 |
. . . . . . . . . 10
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝐴, 𝐵〉, 𝐶〉) |
8 | | vex 3426 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
9 | | vex 3426 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
10 | | vex 3426 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
11 | 8, 9, 10 | otth2 5392 |
. . . . . . . . . 10
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
12 | 7, 11 | bitri 274 |
. . . . . . . . 9
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
13 | 6, 12 | bitrdi 286 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶))) |
14 | 13 | anbi1d 629 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑))) |
15 | | eloprabga.1 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) |
16 | 15 | pm5.32i 574 |
. . . . . . 7
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓)) |
17 | 14, 16 | bitrdi 286 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
18 | 17 | 3exbidv 1929 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
19 | | df-oprab 7259 |
. . . . . . . . 9
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
20 | 19 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝑤 ∈ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)}) |
21 | | abid 2719 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
22 | 20, 21 | bitr2i 275 |
. . . . . . 7
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) |
23 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → (𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
24 | 22, 23 | syl5bb 282 |
. . . . . 6
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
25 | 24 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
26 | | 19.41vvv 1956 |
. . . . . . 7
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓)) |
27 | | elisset 2820 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴) |
28 | | elisset 2820 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V → ∃𝑦 𝑦 = 𝐵) |
29 | | elisset 2820 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V → ∃𝑧 𝑧 = 𝐶) |
30 | 27, 28, 29 | 3anim123i 1149 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
31 | | 3exdistr 1965 |
. . . . . . . . . . 11
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ ∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))) |
32 | | 19.41v 1954 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))) |
33 | | 19.41v 1954 |
. . . . . . . . . . . 12
⊢
(∃𝑦(𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶) ↔ (∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
34 | 33 | anbi2i 622 |
. . . . . . . . . . 11
⊢
((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) ↔ (∃𝑥 𝑥 = 𝐴 ∧ (∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))) |
35 | 31, 32, 34 | 3bitri 296 |
. . . . . . . . . 10
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ (∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))) |
36 | | 3anass 1093 |
. . . . . . . . . 10
⊢
((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ (∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))) |
37 | 35, 36 | bitr4i 277 |
. . . . . . . . 9
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
38 | 30, 37 | sylibr 233 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → ∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
39 | 38 | biantrurd 532 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝜓 ↔ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
40 | 26, 39 | bitr4id 289 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓)) |
41 | 40 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓)) |
42 | 18, 25, 41 | 3bitr3d 308 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
43 | 42 | expcom 413 |
. . 3
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓))) |
44 | 4, 43 | vtocle 3514 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) →
(〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
45 | 1, 2, 3, 44 | syl3an 1158 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |