| 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 5658 | . . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
| 2 | ssel2 3934 | . . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) | |
| 3 | 1, 2 | sylanb 592 | . 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) |
| 4 | 1st2nd2 8013 | . 2 ⊢ (𝐴 ∈ (V × V) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | |
| 5 | 3, 4 | syl 18 | 1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 Vcvv 3457 ⊆ wss 3907 〈cop 4591 × cxp 5649 Rel wrel 5656 ‘cfv 6525 1st c1st 7972 2nd c2nd 7973 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6481 df-fun 6527 df-fv 6533 df-1st 7974 df-2nd 7975 |
| This theorem is referenced by: 2ndrn 8026 1st2ndbr 8027 funfv1st2nd 8031 funelss 8032 elopabi 8047 cnvf1olem 8093 ordpinq 10916 addassnq 10931 mulassnq 10932 distrnq 10934 mulidnq 10936 recmulnq 10937 ltexnq 10948 fsumcnv 15812 fprodcnv 16025 cofulid 17935 cofurid 17936 idffth 17980 cofull 17981 cofth 17982 ressffth 17985 isnat2 17996 nat1st2nd 17999 homadmcd 18087 catciso 18156 prf1st 18248 prf2nd 18249 1st2ndprf 18250 curfuncf 18282 uncfcurf 18283 curf2ndf 18291 yonffthlem 18326 yoniso 18329 dprd2dlem2 20100 dprd2dlem1 20101 dprd2da 20102 mdetunilem9 22734 2ndcctbss 23569 utop2nei 24364 utop3cls 24365 caubl 25424 wlkop 29882 nvop2 30865 nvvop 30866 nvop 30933 phop 31075 fgreu 32924 1stpreimas 32959 gsumhashmul 33295 cvmliftlem1 35643 heiborlem3 38319 rngoi 38405 drngoi 38457 isdrngo1 38462 iscrngo2 38503 tposideq 49518 cic1st2nd 49677 cofu1st2nd 49722 oppfval2 49767 oppfoppc2 49772 idfth 49788 up1st2nd 49815 up1st2ndr 49816 uptrlem2 49841 uptra 49845 uobeqw 49849 uobeq 49850 uptr2a 49852 diag1 49934 fuco11bALT 49968 fuco22nat 49976 fucocolem4 49986 precofvalALT 49998 prcoftposcurfucoa 50014 prcofdiag1 50023 prcofdiag 50024 oppfdiag1 50044 oppfdiag 50046 termcfuncval 50162 diagffth 50168 lmddu 50297 |
| Copyright terms: Public domain | W3C validator |