![]() |
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 5689 | . . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
2 | ssel2 3974 | . . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) | |
3 | 1, 2 | sylanb 579 | . 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) |
4 | 1st2nd2 8042 | . 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 394 = wceq 1534 ∈ wcel 2099 Vcvv 3462 ⊆ wss 3947 〈cop 4639 × cxp 5680 Rel wrel 5687 ‘cfv 6554 1st c1st 8001 2nd c2nd 8002 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-iota 6506 df-fun 6556 df-fv 6562 df-1st 8003 df-2nd 8004 |
This theorem is referenced by: 2ndrn 8055 1st2ndbr 8056 funfv1st2nd 8060 funelss 8061 elopabi 8076 cnvf1olem 8124 ordpinq 10986 addassnq 11001 mulassnq 11002 distrnq 11004 mulidnq 11006 recmulnq 11007 ltexnq 11018 fsumcnv 15777 fprodcnv 15985 cofulid 17909 cofurid 17910 idffth 17955 cofull 17956 cofth 17957 ressffth 17960 isnat2 17971 nat1st2nd 17974 homadmcd 18064 catciso 18133 prf1st 18228 prf2nd 18229 1st2ndprf 18230 curfuncf 18263 uncfcurf 18264 curf2ndf 18272 yonffthlem 18307 yoniso 18310 dprd2dlem2 20040 dprd2dlem1 20041 dprd2da 20042 mdetunilem9 22613 2ndcctbss 23450 utop2nei 24246 utop3cls 24247 caubl 25327 wlkop 29565 nvop2 30541 nvvop 30542 nvop 30609 phop 30751 fgreu 32589 1stpreimas 32617 gsumhashmul 32925 cvmliftlem1 35113 heiborlem3 37514 rngoi 37600 drngoi 37652 isdrngo1 37657 iscrngo2 37698 |
Copyright terms: Public domain | W3C validator |