Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opth | Structured version Visualization version GIF version |
Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.) |
Ref | Expression |
---|---|
opth1.1 | ⊢ 𝐴 ∈ V |
opth1.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
opth | ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opth1.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | opth1.2 | . . . 4 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | opth1 4870 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 4864 | . . . . . . 7 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
5 | id 22 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
6 | 4, 5 | syl5eleq 2694 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
7 | oprcl 4365 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
8 | 6, 7 | syl 17 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 478 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐷 ∈ V) |
10 | 3 | opeq1d 4346 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) |
11 | 10, 5 | eqtr3d 2646 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) |
12 | 8 | simpld 474 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
13 | dfopg 4338 | . . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) | |
14 | 12, 2, 13 | sylancl 693 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2646 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐵}}) |
16 | dfopg 4338 | . . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
17 | 8, 16 | syl 17 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2646 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | prex 4836 | . . . . . 6 ⊢ {𝐶, 𝐵} ∈ V | |
20 | prex 4836 | . . . . . 6 ⊢ {𝐶, 𝐷} ∈ V | |
21 | 19, 20 | preqr2 4321 | . . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷}) |
22 | 18, 21 | syl 17 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐶, 𝐵} = {𝐶, 𝐷}) |
23 | preq2 4213 | . . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) | |
24 | 23 | eqeq2d 2620 | . . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | eqeq2 2621 | . . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) | |
26 | 24, 25 | imbi12d 333 | . . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
27 | vex 3176 | . . . . . 6 ⊢ 𝑥 ∈ V | |
28 | 2, 27 | preqr2 4321 | . . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
29 | 26, 28 | vtoclg 3239 | . . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
30 | 9, 22, 29 | sylc 63 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐵 = 𝐷) |
31 | 3, 30 | jca 553 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
32 | opeq12 4342 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
33 | 31, 32 | impbii 198 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 Vcvv 3173 {csn 4125 {cpr 4127 〈cop 4131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 |
This theorem is referenced by: opthg 4872 otth2 4878 copsexg 4882 copsex4g 4885 opcom 4890 moop2 4891 propssopi 4896 opelopabsbALT 4909 ralxpf 5190 cnvcnvsn 5530 funopg 5836 funsndifnop 6321 tpres 6371 oprabv 6601 xpopth 7098 eqop 7099 opiota 7118 soxp 7177 fnwelem 7179 xpdom2 7940 xpf1o 8007 unxpdomlem2 8050 unxpdomlem3 8051 xpwdomg 8373 fseqenlem1 8730 iundom2g 9241 eqresr 9837 cnref1o 11703 hashfun 13084 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 qredeu 15210 qnumdenbi 15290 crth 15321 prmreclem3 15460 imasaddfnlem 16011 dprd2da 18264 dprd2d2 18266 ucnima 21895 numclwlk1lem2f1 26621 br8d 28802 xppreima2 28830 aciunf1lem 28844 ofpreima 28848 erdszelem9 30435 msubff1 30707 mvhf1 30710 brtp 30892 br8 30899 br6 30900 br4 30901 brsegle 31385 poimirlem4 32583 poimirlem9 32588 f1opr 32689 dib1dim 35472 diclspsn 35501 dihopelvalcpre 35555 dihmeetlem4preN 35613 dihmeetlem13N 35626 dih1dimatlem 35636 dihatlat 35641 pellexlem3 36413 pellex 36417 snhesn 37100 opelopab4 37788 av-numclwlk1lem2f1 41524 |
Copyright terms: Public domain | W3C validator |