![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opth1 | Structured version Visualization version GIF version |
Description: Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opth1.1 | ⊢ 𝐴 ∈ V |
opth1.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
opth1 | ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opth1.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | opth1.2 | . . . 4 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | opi1 5479 | . . 3 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
4 | id 22 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
5 | 3, 4 | eleqtrid 2845 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
6 | 1 | sneqr 4845 | . . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶) |
7 | 6 | a1i 11 | . . 3 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶} → 𝐴 = 𝐶)) |
8 | oprcl 4904 | . . . . . . 7 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
9 | 8 | simpld 494 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
10 | prid1g 4765 | . . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷}) | |
11 | 9, 10 | syl 17 | . . . . 5 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 𝐶 ∈ {𝐶, 𝐷}) |
12 | eleq2 2828 | . . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷})) | |
13 | 11, 12 | syl5ibrcom 247 | . . . 4 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴})) |
14 | elsni 4648 | . . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴) | |
15 | 14 | eqcomd 2741 | . . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶) |
16 | 13, 15 | syl6 35 | . . 3 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶)) |
17 | id 22 | . . . . 5 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) | |
18 | dfopg 4876 | . . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
19 | 8, 18 | syl 17 | . . . . 5 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
20 | 17, 19 | eleqtrd 2841 | . . . 4 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}}) |
21 | elpri 4654 | . . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷})) | |
22 | 20, 21 | syl 17 | . . 3 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷})) |
23 | 7, 16, 22 | mpjaod 860 | . 2 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
24 | 5, 23 | syl 17 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1537 ∈ wcel 2106 Vcvv 3478 {csn 4631 {cpr 4633 〈cop 4637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 |
This theorem is referenced by: opth 5487 dmsnopg 6235 funcnvsn 6618 oprabidw 7462 oprabid 7463 seqomlem2 8490 unxpdomlem3 9286 dfac5lem4 10164 dfac5lem4OLD 10166 dcomex 10485 canthwelem 10688 uzrdgfni 13996 fnpr2ob 17605 gsum2d2 20007 noseqrdgfn 28327 poimirlem9 37616 ichnreuop 47397 ichreuopeq 47398 |
Copyright terms: Public domain | W3C validator |