![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1st2nd | Structured version Visualization version GIF version |
Description: Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.) |
Ref | Expression |
---|---|
1st2nd | ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rel 5256 | . . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
2 | ssel2 3745 | . . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) | |
3 | 1, 2 | sylanb 562 | . 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) |
4 | 1st2nd2 7353 | . 2 ⊢ (𝐴 ∈ (V × V) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | |
5 | 3, 4 | syl 17 | 1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 = wceq 1630 ∈ wcel 2144 Vcvv 3349 ⊆ wss 3721 〈cop 4320 × cxp 5247 Rel wrel 5254 ‘cfv 6031 1st c1st 7312 2nd c2nd 7313 |
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-8 2146 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-pow 4971 ax-pr 5034 ax-un 7095 |
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-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-rab 3069 df-v 3351 df-sbc 3586 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 df-uni 4573 df-br 4785 df-opab 4845 df-mpt 4862 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-iota 5994 df-fun 6033 df-fv 6039 df-1st 7314 df-2nd 7315 |
This theorem is referenced by: 2ndrn 7364 1st2ndbr 7365 elopabi 7380 cnvf1olem 7425 ordpinq 9966 addassnq 9981 mulassnq 9982 distrnq 9984 mulidnq 9986 recmulnq 9987 ltexnq 9998 fsumcnv 14711 fprodcnv 14919 cofulid 16756 cofurid 16757 idffth 16799 cofull 16800 cofth 16801 ressffth 16804 isnat2 16814 nat1st2nd 16817 homadmcd 16898 catciso 16963 prf1st 17051 prf2nd 17052 1st2ndprf 17053 curfuncf 17085 uncfcurf 17086 curf2ndf 17094 yonffthlem 17129 yoniso 17132 dprd2dlem2 18646 dprd2dlem1 18647 dprd2da 18648 mdetunilem9 20643 2ndcctbss 21478 utop2nei 22273 utop3cls 22274 caubl 23324 wlkop 26757 nvop2 27797 nvvop 27798 nvop 27865 phop 28007 fgreu 29805 1stpreimas 29817 cvmliftlem1 31599 heiborlem3 33937 rngoi 34023 drngoi 34075 isdrngo1 34080 iscrngo2 34121 |
Copyright terms: Public domain | W3C validator |