![]() |
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 5442 | . . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V)) | |
2 | ssel2 3879 | . . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) | |
3 | 1, 2 | sylanb 581 | . 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V)) |
4 | 1st2nd2 7575 | . 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 396 = wceq 1520 ∈ wcel 2079 Vcvv 3432 ⊆ wss 3854 〈cop 4472 × cxp 5433 Rel wrel 5440 ‘cfv 6217 1st c1st 7534 2nd c2nd 7535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-sbc 3702 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-iota 6181 df-fun 6219 df-fv 6225 df-1st 7536 df-2nd 7537 |
This theorem is referenced by: 2ndrn 7587 1st2ndbr 7588 funfv1st2nd 7592 funelss 7593 elopabi 7607 cnvf1olem 7652 ordpinq 10200 addassnq 10215 mulassnq 10216 distrnq 10218 mulidnq 10220 recmulnq 10221 ltexnq 10232 fsumcnv 14949 fprodcnv 15158 cofulid 16977 cofurid 16978 idffth 17020 cofull 17021 cofth 17022 ressffth 17025 isnat2 17035 nat1st2nd 17038 homadmcd 17119 catciso 17184 prf1st 17271 prf2nd 17272 1st2ndprf 17273 curfuncf 17305 uncfcurf 17306 curf2ndf 17314 yonffthlem 17349 yoniso 17352 dprd2dlem2 18867 dprd2dlem1 18868 dprd2da 18869 mdetunilem9 20901 2ndcctbss 21735 utop2nei 22530 utop3cls 22531 caubl 23582 wlkop 27080 nvop2 28064 nvvop 28065 nvop 28132 phop 28274 fgreu 30080 1stpreimas 30102 cvmliftlem1 32096 heiborlem3 34569 rngoi 34655 drngoi 34707 isdrngo1 34712 iscrngo2 34753 |
Copyright terms: Public domain | W3C validator |