Step | Hyp | Ref
| Expression |
1 | | elex 2741 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | elex 2741 |
. 2
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
3 | | elex 2741 |
. 2
⊢ (𝐶 ∈ 𝑋 → 𝐶 ∈ V) |
4 | | opexg 4211 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 ∈ V) |
5 | | opexg 4211 |
. . . . 5
⊢
((〈𝐴, 𝐵〉 ∈ V ∧ 𝐶 ∈ V) →
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V) |
6 | 4, 5 | sylan 281 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V) →
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V) |
7 | 6 | 3impa 1189 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) →
〈〈𝐴, 𝐵〉, 𝐶〉 ∈ V) |
8 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) |
9 | 8 | eqeq1d 2179 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
10 | | eqcom 2172 |
. . . . . . . . . . 11
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝐴, 𝐵〉, 𝐶〉) |
11 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
12 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
13 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
14 | 11, 12, 13 | otth2 4224 |
. . . . . . . . . . 11
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
15 | 10, 14 | bitri 183 |
. . . . . . . . . 10
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
16 | 9, 15 | bitrdi 195 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶))) |
17 | 16 | anbi1d 462 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑))) |
18 | | eloprabga.1 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) |
19 | 18 | pm5.32i 451 |
. . . . . . . 8
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓)) |
20 | 17, 19 | bitrdi 195 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
21 | 20 | 3exbidv 1862 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
22 | | df-oprab 5854 |
. . . . . . . . . 10
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
23 | 22 | eleq2i 2237 |
. . . . . . . . 9
⊢ (𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝑤 ∈ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)}) |
24 | | abid 2158 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} ↔ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
25 | 23, 24 | bitr2i 184 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) |
26 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → (𝑤 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
27 | 25, 26 | syl5bb 191 |
. . . . . . 7
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
28 | 27 | adantl 275 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑})) |
29 | | 19.41vvv 1897 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓)) |
30 | | elisset 2744 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴) |
31 | | elisset 2744 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → ∃𝑦 𝑦 = 𝐵) |
32 | | elisset 2744 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ V → ∃𝑧 𝑧 = 𝐶) |
33 | 30, 31, 32 | 3anim123i 1179 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
34 | | eeeanv 1926 |
. . . . . . . . . 10
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
35 | 33, 34 | sylibr 133 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → ∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶)) |
36 | 35 | biantrurd 303 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝜓 ↔ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓))) |
37 | 29, 36 | bitr4id 198 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓)) |
38 | 37 | adantr 274 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓)) |
39 | 21, 28, 38 | 3bitr3d 217 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
40 | 39 | expcom 115 |
. . . 4
⊢ (𝑤 = 〈〈𝐴, 𝐵〉, 𝐶〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓))) |
41 | 40 | vtocleg 2801 |
. . 3
⊢
(〈〈𝐴,
𝐵〉, 𝐶〉 ∈ V → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓))) |
42 | 7, 41 | mpcom 36 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) →
(〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
43 | 1, 2, 3, 42 | syl3an 1275 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |