![]() |
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 5064 | . . 3 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
4 | id 22 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
5 | 3, 4 | syl5eleq 2855 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
6 | 1 | sneqr 4502 | . . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶) |
7 | 6 | a1i 11 | . . 3 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶} → 𝐴 = 𝐶)) |
8 | oprcl 4563 | . . . . . . 7 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
9 | 8 | simpld 476 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
10 | prid1g 4429 | . . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷}) | |
11 | 9, 10 | syl 17 | . . . . 5 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 𝐶 ∈ {𝐶, 𝐷}) |
12 | eleq2 2838 | . . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷})) | |
13 | 11, 12 | syl5ibrcom 237 | . . . 4 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴})) |
14 | elsni 4331 | . . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴) | |
15 | 14 | eqcomd 2776 | . . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶) |
16 | 13, 15 | syl6 35 | . . 3 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶)) |
17 | id 22 | . . . . 5 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) | |
18 | dfopg 4535 | . . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
19 | 8, 18 | syl 17 | . . . . 5 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
20 | 17, 19 | eleqtrd 2851 | . . . 4 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}}) |
21 | elpri 4335 | . . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷})) | |
22 | 20, 21 | syl 17 | . . 3 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷})) |
23 | 7, 16, 22 | mpjaod 840 | . 2 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
24 | 5, 23 | syl 17 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∨ wo 826 = wceq 1630 ∈ wcel 2144 Vcvv 3349 {csn 4314 {cpr 4316 〈cop 4320 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-sep 4912 ax-nul 4920 ax-pr 5034 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-v 3351 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 |
This theorem is referenced by: opth 5072 dmsnopg 5748 funcnvsn 6079 oprabid 6821 seqomlem2 7698 unxpdomlem3 8321 dfac5lem4 9148 dcomex 9470 canthwelem 9673 uzrdgfni 12964 gsum2d2 18579 poimirlem9 33744 |
Copyright terms: Public domain | W3C validator |