Step | Hyp | Ref
| Expression |
1 | | opth1.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | | opth1.2 |
. . . 4
⊢ 𝐵 ∈ V |
3 | 1, 2 | opth1 4236 |
. . 3
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 4232 |
. . . . . . 7
⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩ |
5 | | id 19 |
. . . . . . 7
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩) |
6 | 4, 5 | eleqtrid 2266 |
. . . . . 6
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩) |
7 | | oprcl 3802 |
. . . . . 6
⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
8 | 6, 7 | syl 14 |
. . . . 5
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 114 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V) |
10 | 3 | opeq1d 3784 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩) |
11 | 10, 5 | eqtr3d 2212 |
. . . . . . 7
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩) |
12 | 8 | simpld 112 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V) |
13 | | dfopg 3776 |
. . . . . . . 8
⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}}) |
14 | 12, 2, 13 | sylancl 413 |
. . . . . . 7
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2212 |
. . . . . 6
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}}) |
16 | | dfopg 3776 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}}) |
17 | 8, 16 | syl 14 |
. . . . . 6
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2212 |
. . . . 5
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | | prexg 4211 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → {𝐶, 𝐵} ∈ V) |
20 | 12, 2, 19 | sylancl 413 |
. . . . . 6
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} ∈ V) |
21 | | prexg 4211 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → {𝐶, 𝐷} ∈ V) |
22 | 8, 21 | syl 14 |
. . . . . 6
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐷} ∈ V) |
23 | | preqr2g 3767 |
. . . . . 6
⊢ (({𝐶, 𝐵} ∈ V ∧ {𝐶, 𝐷} ∈ V) → ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})) |
24 | 20, 22, 23 | syl2anc 411 |
. . . . 5
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | 18, 24 | mpd 13 |
. . . 4
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷}) |
26 | | preq2 3670 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) |
27 | 26 | eqeq2d 2189 |
. . . . . 6
⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
28 | | eqeq2 2187 |
. . . . . 6
⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) |
29 | 27, 28 | imbi12d 234 |
. . . . 5
⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
30 | | vex 2740 |
. . . . . 6
⊢ 𝑥 ∈ V |
31 | 2, 30 | preqr2 3769 |
. . . . 5
⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
32 | 29, 31 | vtoclg 2797 |
. . . 4
⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
33 | 9, 25, 32 | sylc 62 |
. . 3
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷) |
34 | 3, 33 | jca 306 |
. 2
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
35 | | opeq12 3780 |
. 2
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩) |
36 | 34, 35 | impbii 126 |
1
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |